equiv_equivalence
plain-language theorem explainer
The pointwise-convergence-to-zero relation on regular sequences of δ-rationals is an equivalence relation. Anyone assembling the M0a constructive real line cites this to obtain a genuine setoid, choice-free. The proof is a term-mode record packing the already-proved reflexive, symmetric, and transitive lemmas.
Claim. The relation $\sim$ on regular sequences of $\delta$-rationals, where $s \sim t$ means that for every tolerance $1/(k+1)$ one has eventually $|s_n-t_n|\le 1/(k+1)$ (measured via integer cross-differences and denominator products), is an equivalence relation: reflexive, symmetric, and transitive.
background
M0a builds a constructive real line from regular sequences of δ-rationals. A regular sequence is a sequence of δ-rationals with a modulus controlling how fast consecutive terms settle; the working equality equiv declares two such sequences equal when their pointwise difference converges to zero in the explicit sense that for every $k$ there is $N$ so that for all $n\ge N$, the absolute cross-difference times $(k+1)$ is at most the product of the two denominators.
That cross-difference is the integer numerator of the formal difference of two δ-rationals, so the whole relation lives on integers and natural numbers and never needs classical $\mathbb{Q}$ display. Upstream, reflexivity is immediate from vanishing self-difference; symmetry follows because swapping arguments only flips the sign of the cross-difference; transitivity is a choice-free triangle argument that tightens the tolerance to $1/(2k+2)$ on each leg and reassembles via a three-point identity.
The local goal is to finish the setoid structure so that the quotient (built with Quot only) becomes the pre-real line $\mathbb{R}^\delta_{\mathrm{pre}}$, with the constant-sequence map $\eta$ descending to a rational embedding.
proof idea
Term-mode construction of the Equivalence record. The three fields are filled by direct application of the already-proved lemmas: reflexivity from the self-difference vanishing, symmetry from sign-flip invariance of the absolute cross-difference, and transitivity from the integer-level triangle argument at doubled tolerance. No new arithmetic is done here; the theorem only packages those three facts into the structure Lean’s setoid API expects.
why it matters
This is the last glue step before the M0a real setoid: the downstream definition installs equiv as the relation and cites this theorem as iseqv, so the quotient carrier is well-defined. That setoid is exactly the constructive real line $\mathbb{R}^\delta_{\mathrm{pre}}$; the constant-sequence embedding $\eta$ then descends, and injectivity of the descended map (no two distinct δ-rationals collapse) is proved from the same equivalence. In the broader Recognition foundation this keeps the real completion inside {propext, Quot.sound}, matching the choice-free integer and rational layers built earlier by Grothendieck completion of logic-native naturals. It does not yet address completeness or field operations; those sit on top of the setoid.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.