equiv_trans
plain-language theorem explainer
Transitivity of working equality on regular sequences of delta-rationals: if s is eventually within every 1/(k+1) of t and t of u, then s is of u. Cited by anyone assembling the M0a real setoid. The proof is a choice-free triangle at the integer cross-multiplication level, feeding two 1/(2k+2) bounds through the three-point identity and cancelling the positive middle denominator.
Claim. Let $s,t,u$ be regular sequences of delta-rationals. Suppose that for every $k\in\mathbb{N}$ one has eventually $|s_n-t_n|\le 1/(k+1)$ and eventually $|t_n-u_n|\le 1/(k+1)$, both expressed via integer cross-multiplication (no $\mathbb{Q}$ display). Then for every $k$ one has eventually $|s_n-u_n|\le 1/(k+1)$.
background
This module builds the M0a carrier for a choice-free real completion: regular sequences of delta-rationals, equated when their pointwise difference tends to zero. A sequence $(a_n)$ is regular when $|a_m-a_n|\le 1/(m+1)+1/(n+1)$ for all indices, written entirely with integer cross-multiplication so that $|\mathrm{crossDiff}(a_m,a_n)|\cdot(m+1)\cdot(n+1)\le(m+n+2),\mathrm{den}(a_m),\mathrm{den}(a_n)$.
Working equality of two regular sequences means: for every tolerance $1/(k+1)$, eventually the cross-diff bound $|s_n-t_n|\le 1/(k+1)$ holds. Reflexivity and symmetry are already available; the missing piece for a setoid is transitivity.
The local arithmetic stays on the integer side (natAbs of crossDiff, denominator toNat maps, Nat inequalities). Upstream support includes ordinary Nat/Int lemmas such as le_trans and positivity of denominators; the key algebraic input is the three-point identity relating crossDiff of $(A,C)$ to the sum of the $(A,B)$ and $(B,C)$ terms scaled by the third denominator.
proof idea
Fix tolerance index $k$. Apply the two hypotheses at the stricter level $2k+1$, obtaining thresholds $N_1,N_2$. Past $\max(N_1,N_2)$, write $A=s_n$, $B=t_n$, $C=u_n$. The hypotheses give $\mathrm{natAbs}(\mathrm{crossDiff},A,B)\cdot(2k+2)\le\mathrm{den}(A),\mathrm{den}(B)$ and likewise for $B,C$.
Invoke the integer identity $\mathrm{crossDiff}(A,C)\cdot\mathrm{den}(B)=\mathrm{crossDiff}(A,B)\cdot\mathrm{den}(C)+\mathrm{crossDiff}(B,C)\cdot\mathrm{den}(A)$. Pass to natAbs, use the triangle inequality for natAbs of a sum, and clear casts. The rest is pure Nat arithmetic: multiply the triangle by $2k+2$, substitute the two hypothesis bounds, expand, rewrite $2k+2=2(k+1)$, factor $2,\mathrm{den}(B)$ on both sides, and cancel that positive factor to obtain the target bound at level $k$. No classical choice and no $\mathbb{Q}$ coercion.
why it matters
This is the hard leg of the equivalence relation on regular sequences. Downstream, equiv_equivalence packages reflexivity, symmetry, and this transitivity into a genuine Equivalence, completing the M0a carrier into a setoid of reals built from delta-rationals.
In the Recognition Science foundation stack, M0a is the first growth step of the primitive recognition calculus: a choice-free real line on which later cost, forcing, and ladder constructions sit. Keeping the proof inside {propext, Quot.sound} (no classical choice, no $\mathbb{Q}$ display) matches the project's constraint that the arithmetic substrate not smuggle classical axioms into the forcing chain.
Without transitivity the setoid does not form, and the unit map from delta-rationals into the completion cannot be well-defined up to equivalence. The sibling well-definedness fact (eta respects cross-equality) sits next to this result in the same module.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.