etaQ
plain-language theorem explainer
The unit map η sends each δ-rational to the constructive real given by its constant regular sequence. Anyone building the M0a real line or the Forced ⊣ Classical adjunction cites this carrier morphism. Well-definedness is a single Quot.lift using that cross-equal ratio orbits yield equivalent constant sequences.
Claim. The unit map $\eta:\mathbb{Q}_\delta\to\mathbb{R}_\delta^{\mathrm{pre}}$ sends a PRC rational (a ratio-orbit class modulo cross-equality) to the equivalence class of the constant regular sequence at any representative. If two ratio orbits are cross-equal, their constant sequences are equivalent, so the map descends through both quotients.
background
In the Primitive Recognition Calculus, δ-rationals are ratio orbits of integers identified by cross-multiplication (cross-equality). PRCRat is that quotient. The M0a constructive real line RealDelta is regular sequences of such δ-rationals, modulo sequences that converge pointwise to zero; the carrier is a bare Quot, so it lives on the FORCED audit tier {propext, Quot.sound}.
The pre-quotient unit eta embeds a single ratio orbit as the constant regular sequence at that orbit. The key upstream fact is that eta respects cross-equality: cross-equal orbits give equivalent constant sequences (their cross-difference vanishes identically). Equivalent regular sequences determine equal constructive reals via Quot.sound.
This module sits in the Grow/EtaCompletionM0a layer: building the unit of the Forced ⊣ Classical adjunction at the level of carriers, before order and field structure.
proof idea
One-line definition by Quot.lift. On a ratio-orbit display q, send it to RealDelta.mk (eta q), the class of the constant regular sequence. The lift obligation is discharged by eta_respects_crossEq plus mk_eq_mk_of_equiv: if two orbits are cross-equal, their constant sequences are equivalent, hence determine the same constructive real. No further arithmetic is needed.
why it matters
This is the M0a carrier morphism of the Forced ⊣ Classical adjunction program: the unit that embeds the δ-rational base into the choice-free constructive real line. Downstream, etaQ_mk records the display equation (η on a constructor is the class of the constant sequence), and etaQ_injective proves the unit is injective, so distinct δ-rationals do not collapse in the completion.
Together those facts make η a genuine embedding of the rational base into ℝδ_pre. That embedding is the starting point for Archimedean comparison, order, and the rest of the completion stack that feeds Recognition Science's constructive number line without classical choice.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.