etaQ_mk
plain-language theorem explainer
On a display ratio orbit q, the unit map η from δ-rationals into the M0a pre-reals sends the quotient class of q to the class of the constant regular sequence at q. Anyone simplifying expressions involving η on concrete rationals will cite this simp lemma. The proof is pure definitional equality (rfl) from the Quot.lift presentation of η.
Claim. For every display ratio orbit $q$, the unit map $\eta:\mathbb{Q}_\delta\to\mathbb{R}^\delta_{\mathrm{pre}}$ satisfies $\eta([q])=[(\eta q)]$, where $[q]$ is the PRC-rational class of $q$ and $(\eta q)$ is the constant regular sequence with value $q$.
background
Module EtaCompletionM0a builds the M0a constructive real line $\mathbb{R}^\delta_{\mathrm{pre}}$ as regular sequences of $\delta$-rationals modulo pointwise convergence to zero, using only Quot (audit tier FORCED on {propext, Quot.sound}).
The unit map eta embeds a ratio orbit $q$ as the constant regular sequence $n\mapsto q$. The descended map etaQ sends a PRC rational (ratio orbit modulo cross-equality) to the RealDelta class of that constant sequence; well-definedness rests on eta_respects_crossEq. PRCRat.mk and RealDelta.mk are the respective quotient constructors.
This lemma records the interaction of those two constructors with the lift defining etaQ.
proof idea
One-line term proof by rfl. By definition etaQ is Quot.lift (fun q => RealDelta.mk (eta q)) ..., so on a display PRCRat.mk q the lift reduces definitionally to RealDelta.mk (eta q). No lemmas are applied beyond the definitional unfolding of the lift.
why it matters
This is the computational face of the M0a carrier morphism of the Forced ⊣ Classical adjunction program: $\eta:\mathbb{Q}\delta\to\mathbb{R}^\delta{\mathrm{pre}}$ on concrete displays. Marked @[simp], it keeps goal states in normal form when later lemmas reason about Archimedean comparison, cross-equality, or completion of the $\delta$-rationals.
No downstream dependents are wired yet (used_by_count = 0), so the lemma is infrastructure for the grow/completion stack rather than a cited parent theorem. It sits upstream of any uniqueness or density arguments that identify constant sequences with embedded rationals inside the constructive reals used by the Primitive Recognition Calculus.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.