RealDelta
plain-language theorem explainer
The M0a constructive real line is the quotient of regular sequences of δ-rationals by pointwise convergence to zero. Anyone citing the rational embedding η or the Forced ⊣ Classical adjunction carrier will land here. The definition is a one-line Quot of the M0a setoid, so the type sits only on propext and Quot.sound (audit tier FORCED).
Claim. Define the M0a constructive real line by $\mathbb{R}^\delta_{\mathrm{pre}} := \mathrm{Quot}(\sim)$, where $\sim$ is the setoid on regular sequences of $\delta$-rationals whose relation is pointwise convergence of the difference to zero.
background
M0a builds a choice-free real line inside the Primitive Recognition Calculus grow path. A regular sequence is a sequence of δ-rationals with a controlled Cauchy modulus. Two sequences are equivalent when their difference tends pointwise to zero in the δ-rational order; that relation, with its equivalence proof, is packaged as the M0a setoid.
The carrier is formed with Quot alone, avoiding classical choice and heavier quotient APIs, so the audit footprint is exactly {propext, Quot.sound}. Upstream, the setoid is defined by taking the relation to be that equivalence and supplying the equivalence proof. The broader foundation bridge from the ledger floor toward classical structure remains an open task at higher levels; this module only installs the pre-real carrier.
proof idea
One-line definition: the type is Quot of the M0a setoid on regular sequences. No further data. The ensuing namespace exposes the standard quotient interface (constructor via Quot.mk, and equality of classes from related representatives via Quot.sound).
why it matters
This type is the codomain of the unit map η from δ-rationals into the M0a reals: a PRC rational maps to the class of its constant regular sequence. Downstream, injectivity of that unit shows distinct δ-rationals do not collapse, and the simp lemma on display rationals identifies η of a class with the class of the constant sequence.
In the Forced ⊣ Classical adjunction program this is the M0a carrier morphism's target. It supplies a constructive continuum in the foundation grow path before the forcing chain forces phi, the eight-tick octave, and D = 3. Keeping the quotient choice-free is intentional: the recognition calculus stays on a minimal axiom base while the rational embedding is installed.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.