equiv_refl
plain-language theorem explainer
Every regular sequence of δ-rationals is equivalent to itself under the working equality that demands pointwise differences vanish at every positive tolerance. Builders of the M0a real setoid cite this for the reflexive leg. The argument is short: the self cross-difference is identically zero, so the absolute-value bound holds from index N = 0 onward.
Claim. Let $s$ be a regular sequence of $\delta$-rationals. Then $s$ is equivalent to itself: for every tolerance index $k\in\mathbb{N}$ there exists $N$ such that for all $n\ge N$, $\lvert s_n-s_n\rvert\le 1/(k+1)$ in the cross-multiplication sense (the absolute cross-difference times the denominator product is at most the scaled product of denominators).
background
The module builds a choice-free completion of the M0a carrier from regular sequences of δ-rationals. A sequence $(a_n)$ is regular when the integer cross-difference satisfies $\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)$ for all indices, the display-free form of $\lvert a_m-a_n\rvert\le 1/(m+1)+1/(n+1)$.
Working equality of two regular sequences means their pointwise difference tends to zero: for every tolerance $1/(k+1)$ there is an $N$ past which $\lvert s_n-t_n\rvert\le 1/(k+1)$, again via cross-multiplication. The sibling fact that the cross-difference of any ratio-orbit with itself is zero is the algebraic input used here.
Upstream arithmetic supplies the elementary facts $0\le n$ and $0\cdot n=0$ needed once the absolute value of a zero cross-difference appears.
proof idea
Fix a tolerance index $k$. Witness the eventual bound with $N=0$. For every $n\ge 0$, rewrite the cross-difference of $s_n$ with itself to zero, so its natural absolute value is zero and the left-hand product collapses by $0\cdot m=0$. The resulting inequality $0\le\cdots$ is immediate from non-negativity of naturals. No regularity hypothesis beyond the type is needed for the self-case.
why it matters
This is the reflexive leg of the setoid structure on regular δ-rational sequences. The parent theorem packages reflexivity, symmetry, and transitivity into a single Equivalence, described as "the completion of the M0a carrier into a genuine setoid, all choice-free." Without reflexivity the quotient that supplies M0a reals cannot form. The construction sits in the Primitive Recognition Calculus grow layer, where δ-rationals and regular sequences prepare analytic objects without classical choice, feeding later certified evaluation and cost-side identification with the Recognition J-cost infrastructure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.