mk
plain-language theorem explainer
The canonical map sending a regular sequence of δ-rationals to its class in the M0a constructive real line ℝδ_pre. Anyone building or embedding rationals into ℝδ_pre cites this constructor. The body is the one-line quotient constructor Quot.mk on the regular-sequence setoid.
Claim. Given a regular sequence $s$ of $\delta$-rationals (i.e. $|s_m-s_n|\le 1/(m+1)+1/(n+1)$ for all $m,n$), form the constructive real $[s]\in\mathbb{R}^\delta_{\mathrm{pre}}$ as the equivalence class of $s$ under pointwise convergence to zero.
background
The M0a layer builds a constructive real line before classical reals are available. A regular sequence is a map $n\mapsto a_n$ into $\delta$-rationals (ratio orbits) satisfying the Bishop-style modulus $|a_m-a_n|\le 1/(m+1)+1/(n+1)$, written entirely with integer cross-multiplication so no $\mathbb{Q}$ display is required.
Two regular sequences are equivalent when their pointwise difference tends to zero: for every tolerance $1/(k+1)$ one eventually has $|s_n-t_n|\le 1/(k+1)$. The setoid of that relation yields the carrier $\mathbb{R}^\delta_{\mathrm{pre}}:=\mathrm{Quot}(\mathrm{equivSetoid})$, which sits on the audit tier ${\mathrm{propext},\mathrm{Quot.sound}}$ only.
This constructor is the display map from a concrete regular sequence into that quotient type.
proof idea
One-line definitional wrapper: apply the quotient constructor $\mathrm{Quot.mk}$ to the regular-sequence setoid and the given sequence. No further lemmas are invoked; equality of classes is deferred to the companion soundness lemma for equivalent sequences.
why it matters
Every concrete element of the M0a real line is introduced through this map (or through the rational embedding $\eta$ that factors through it). It is the display half of the quotient presentation of $\mathbb{R}^\delta_{\mathrm{pre}}$, which is the carrier on which later completion, order, and field structure for the primitive recognition calculus are erected. In the Recognition foundation stack this is scaffolding for the real arithmetic underlying cost functionals and the forcing chain, not a physics claim itself. No downstream theorems are recorded yet in the graph; the immediate companion is the statement that equivalent regular sequences determine equal constructive reals.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.