RegularSeq
plain-language theorem explainer
Regular sequences of delta-rationals are the Cauchy-style carriers for the M0a constructive real line. A sequence of ratio-orbits is regular when pairwise differences obey the integer cross-multiplication bound equivalent to |a_m − a_n| ≤ 1/(m+1) + 1/(n+1). Anyone building ℝδ_pre, the rational embedding eta, or the equivalence setoid cites this structure. It is a pure data definition: a sequence field plus the regularity witness.
Claim. A regular sequence is a pair $(a_n)_{n\in\mathbb{N}}$ with each $a_n$ a ratio-orbit (signed numerator over nonzero distinction-nat denominator), together with the regularity witness: for all $m,n$, $\lvert\mathrm{crossDiff}(a_m,a_n)\rvert\cdot(m+1)\cdot(n+1)\le(m+n+2)\cdot\mathrm{den}(a_m)\cdot\mathrm{den}(a_n)$, i.e. $\lvert a_m-a_n\rvert\le 1/(m+1)+1/(n+1)$ without displaying $\mathbb{Q}$.
background
Module EtaCompletionM0a builds a choice-free constructive real line from delta-rationals. The ambient display is RatioOrbit: an integer numerator (SignedOrbit) over a nonzero DistinctionNat denominator. Differences are never formed in ℚ; instead crossDiff supplies the integer numerator of $a-b$, namely $a.\mathrm{num}\cdot b.\mathrm{den}-b.\mathrm{num}\cdot a.\mathrm{den}$. Denominators are read as Lean Nats via toNat on the orbit hierarchy.
Regularity is Bishop-style Cauchy control specialized to the harmonic moduli $1/(n+1)$. The inequality is written entirely with Int.natAbs, crossDiff, and den.toNat so that later setoid proofs stay on {propext, Quot.sound} and never open a rational field display. Constant sequences of a fixed ratio-orbit satisfy the bound (eta_regular), which seeds the unit map into the completion.
proof idea
No proof body: this is a structure declaration. The carrier is seq : ℕ → RatioOrbit plus a Prop field regular asserting the cross-multiplication inequality for every pair of indices. Downstream constructors (notably eta) discharge regular by a separate lemma; consumers pattern-match on the two fields.
why it matters
RegularSeq is the raw carrier before quotienting. Downstream, equiv declares working equality as pointwise crossDiff vanishing in the $1/(k+1)$ tolerance; equiv_refl, equiv_symm, and equiv_trans equip that relation; equivSetoid packages it as a Setoid whose Quot is ℝδ_pre, the M0a constructive real line. The unit map eta embeds each delta-rational as a constant regular sequence, and mk_eq_mk_of_equiv ensures equivalent sequences determine the same real.
In the Recognition foundation this is the first growth step from discrete ratio-orbits toward a continuum on which cost and forcing can act. It is scaffolding for the pre-real line, not yet the full RS real closed field or the J-cost calculus, but it is the setoid substrate those layers will sit on.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.