equiv
plain-language theorem explainer
Working equality of regular δ-rational sequences: their pointwise difference converges to zero. For every tolerance 1/(k+1), eventually |s_n − t_n| ≤ 1/(k+1), encoded by integer cross-multiplication so no ℚ display appears. Anyone assembling the M0a constructive real line cites this as the setoid relation on regular sequences. The body is a bare Prop definition, not a proved theorem.
Claim. Two regular sequences $s$ and $t$ of $\delta$-rationals are equivalent when, for every $k \in \mathbb{N}$, there exists $N$ such that for all $n \geq N$, $|\mathrm{num}(s_n)\,\mathrm{den}(t_n) - \mathrm{num}(t_n)\,\mathrm{den}(s_n)| \cdot (k+1) \leq \mathrm{den}(s_n)\,\mathrm{den}(t_n)$. Equivalently, $|s_n - t_n| \leq 1/(k+1)$ eventually.
background
M0a builds a choice-free constructive real line from δ-rationals (ratio orbits with integer numerator and positive denominator). A sequence $(a_n)$ is regular when $|a_m - a_n| \leq 1/(m+1) + 1/(n+1)$ for all indices; the structure packages the sequence with that inequality written entirely in integer cross-multiplication, avoiding any ℚ display.
The cross-difference of two ratio orbits is the integer numerator of their difference: $a.\mathrm{num}, b.\mathrm{den} - b.\mathrm{num}, a.\mathrm{den}$. Absolute value of that integer, scaled by denominators, replaces ordinary rational distance. The unit map embeds a single δ-rational as a constant regular sequence.
This module sits in the Primitive Recognition Calculus grow path: arithmetic and order on integers are already available, and the goal is a setoid of regular sequences whose quotient is $\mathbb{R}^\delta_{\mathrm{pre}}$.
proof idea
Definitional Prop, not a tactic proof. The body quantifies over tolerances $k$, demands an eventual index $N$, and asserts the scaled cross-difference bound $|\mathrm{crossDiff}(s_n,t_n)|\cdot(k+1) \leq \mathrm{den}(s_n),\mathrm{den}(t_n)$ for all $n \geq N$. That inequality is exactly $|s_n - t_n| \leq 1/(k+1)$ written without rationals. No lemmas are applied; the definition is the relation itself.
why it matters
This is the working equality that turns regular sequences into a setoid. Downstream, reflexivity, symmetry, and the choice-free triangle argument establish that the relation is an equivalence; those three facts assemble into the equivalence package and the setoid instance. The quotient by that setoid is the M0a constructive real line $\mathbb{R}^\delta_{\mathrm{pre}}$, on which the constant-sequence embedding descends to the rational inclusion.
The Archimedean recovery theorem uses the relation on constant sequences: if two constant embeddings are equivalent, their fixed cross-difference lies below every $1/(k+1)$, and instantiating at the product of denominators forces the cross-difference to vanish, hence the underlying δ-rationals are cross-equal. Injectivity of the embedding and respect for cross-equality also route through this definition. In the Recognition foundation stack it supplies the carrier equality for the pre-real line before later forcing steps (T5–T8) attach physical constants.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.