An explicit rational-exponential basis for the universal development quotient

Assume the Axiom of Countable Choice ${\mathrm{A}\mathrm{C}}_{\omega }$ (The Axiom of Countable Choice (${\mathrm{A}\mathrm{C}}_{\omega }$)). Let $Q$ and the member maps $\pi {\mathrm{\mid }}_{U_{\alpha }}:U_{\alpha }\to Q_{\alpha }\subseteq Q$ be as in Existence of a universal development: the quotient of the set-sized family of canonical developments along pairwise maximal common developments clauses (c)-(d): $Q$ is a Hausdorff locally Euclidean smooth four-manifold with a smooth Lorentzian metric $\bar{g}$, the open sets $Q_{\alpha }$ cover $Q$, and each $\pi {\mathrm{\mid }}_{U_{\alpha }}$ is a diffeomorphism onto $Q_{\alpha }$. Let $D\subseteq Q$ be a countable dense subset, as supplied by A countable dense subset of the universal development by rational timelike exponential steps from a dense subset of the initial surface. When $Q$ and $D$ are obtained from these development suppliers, retain their Countable Choice and Dependent Choice hypotheses (The axiom of dependent choice: a relation in which every element is related to something admits an $\mathbb{N}$-indexed chain). The basis construction conditional on the supplied $Q,D$ uses Countable Choice only. Choose one basis at each $d\in D$. In these coordinates let $B_d(a,r)\subseteq T_{d}Q$ be the Euclidean open ball centered at $a\in {\mathbb{Q}}^4$ with radius $r\in {\mathbb{Q}}_{>0}$, and let ${\mathcal{E}}_d$ be the maximal exponential domain. Then $\mathcal{B}:=\{{\exp }_d(B_d(a,r)):d\in D,a\in {\mathbb{Q}}^4,r\in {\mathbb{Q}}_{>0},B_d(a,r)\subseteq {\mathcal{E}}_d,{\exp }_d{\mathrm{\mid }}_{B_d(a,r)}\text{ is a diffeomorphism onto an open subset of }Q\}$ is a countable basis of the topology of $Q$. This exhibits an explicit basis for the second-countability conclusion of Existence of a universal development: the quotient of the set-sized family of canonical developments along pairwise maximal common developments clause (d).

Translated balls are necessary in this construction: after one selects arbitrarily small normal domains at dense centers, their centered subballs need not cover any prescribed point outside $D$. The family above uses all rational translated balls on which the exponential is a diffeomorphism, rather than one selected normal domain per center. The proof gives a general local-exponential countability criterion and does not invoke the conclusion of second countability from the universal-development lemma.