etaQ_injective
plain-language theorem explainer
The unit map from δ-rationals into the M0a pre-real line is injective: distinct rationals never collapse under completion. Anyone assembling the Forced ⊣ Classical adjunction or a choice-free real carrier cites this embedding. The proof peels both quotients, recovers sequence equivalence from class equality via the setoid, then applies the Archimedean cross-equality step.
Claim. The unit $\eta:\mathbb{Q}_\delta\to\mathbb{R}_\delta^{\mathrm{pre}}$ that sends each $\delta$-rational to the equivalence class of its constant regular sequence is injective: if $\eta(q)=\eta(r)$ then $q=r$ in $\mathbb{Q}_\delta$.
background
M0a builds a choice-free pre-real line by completing δ-rationals. A RatioOrbit is a display rational (numerator/denominator data); PRCRat is the quotient of those orbits by cross-equality. A RegularSeq is a sequence of δ-rationals whose consecutive terms stay controlled; two regular sequences are equiv when their pointwise cross-difference falls below every tolerance $1/(k+1)$ eventually. RealDelta is the quotient of regular sequences by that equivalence.
The unit eta embeds a single orbit as the constant regular sequence at that value. Descending through both quotients yields etaQ : PRCRat → RealDelta, the M0a carrier morphism of the Forced ⊣ Classical adjunction program (well-definedness is eta_respects_crossEq).
Upstream, equiv_equivalence makes equiv a genuine setoid, and crossEq_of_equiv_eta is the Archimedean step: if the constant sequences at $q$ and $r$ are equivalent, instantiate the tolerance at $k=\mathrm{den}(q)\cdot\mathrm{den}(r)$ to force the cross-difference coefficient to vanish, hence $q$ and $r$ are cross-equal.
proof idea
Fix $a,b:\mathrm{PRCRat}$ with $\eta_Q(a)=\eta_Q(b)$. Peel both quotients by Quot.ind, reducing to display orbits $q,r$ such that RealDelta.mk (eta q) = RealDelta.mk (eta r). Exactness of the quotient (Quot.eqvGen_exact) yields an EqvGen witness; collapse it with Equivalence.eqvGen_iff equiv_equivalence to obtain equiv (eta q) (eta r). The Archimedean lemma crossEq_of_equiv_eta turns that into cross-equality of $q$ and $r$. Finish by Quot.sound, so $a=b$ in PRCRat.
why it matters
Injectivity plus the already-proved well-definedness of etaQ make the unit a genuine embedding of the rational base into the M0a real line, entirely choice-free. That embedding is the carrier half of the Forced ⊣ Classical adjunction program named in the etaQ doc-comment: without it, δ-rationals could collapse when lifted to pre-reals and the completion would not extend the rational structure faithfully.
No downstream consumers are wired yet in the graph (used_by is empty), so this is presently a leaf that closes the unit-map package inside EtaCompletionM0a. In the broader Recognition foundation it sits under the integers-and-rationals-from-logic stack (IntegersFromLogic.sound, RationalsFromLogic.sound) and supplies the rational spine that later forcing steps (T5–T8, the φ-ladder, eight-tick structure) will inhabit once the real carrier is fully assembled.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.