crossDiff_triangle_id
plain-language theorem explainer
For three ratio orbits, the integer cross-difference of the outer pair, scaled by the middle denominator, equals the sum of the two adjacent cross-differences each scaled by the remaining denominator. Anyone proving transitivity of regular-sequence equivalence at the integer level cites this identity. The proof is a one-line unfold-and-ring reduction of the cross-difference definition.
Claim. For ratio orbits $a,b,c$ with integer numerators and positive integer denominators, writing $\Delta(x,y):=x_{\mathrm{num}}\,y_{\mathrm{den}}-y_{\mathrm{num}}\,x_{\mathrm{den}}$, one has $\Delta(a,c)\,b_{\mathrm{den}}=\Delta(a,b)\,c_{\mathrm{den}}+\Delta(b,c)\,a_{\mathrm{den}}$.
background
In the primitive recognition calculus, rationals are carried as ratio orbits: a signed integer numerator paired with a positive natural denominator, without descending to Mathlib's $\mathbb{Q}$. The cross-difference of two orbits is the integer numerator of their difference, $\Delta(a,b)=a_{\mathrm{num}}b_{\mathrm{den}}-b_{\mathrm{num}}a_{\mathrm{den}}$. All later estimates stay on pure integer arithmetic (and on the axiom set ${\mathrm{propext},\mathrm{Quot.sound}}$).
The surrounding module builds an $\eta$-completion: regular sequences of these delta-rationals, with regularity stated by a cross-multiplication bound that avoids rational display. Equivalence of two regular sequences is eventual smallness of their cross-differences. Transitivity needs a three-point identity mirroring $(a-c)=(a-b)+(b-c)$ after clearing denominators.
Clearing the three denominators and rearranging yields exactly the stated integer identity.
proof idea
Unfold the definition of cross-difference on both sides. After substituting $\Delta(x,y)=x_{\mathrm{num}}y_{\mathrm{den}}-y_{\mathrm{num}}x_{\mathrm{den}}$, both sides become identical bilinear polynomials in the six integer components (three numerators, three denominators). The ring tactic closes the equality. No upstream lemmas are required; it is a pure algebraic identity.
why it matters
This identity is the algebraic backbone of the triangle inequality for regular sequences. Downstream, transitivity of regular-sequence equivalence applies it (with positivity of the middle denominator) to pass from eventual bounds $|s_n-t_n|\le 1/(2k+2)$ and $|t_n-u_n|\le 1/(2k+2)$ to $|s_n-u_n|\le 1/(k+1)$, staying entirely at the integer cross-multiplication level.
That choice-free transitivity makes the equivalence relation on regular sequences well-defined without a $\mathbb{Q}$ display, which is the point of the EtaCompletionM0a development: construct the completion (reals as regular sequences of recognition rationals) on a minimal logical base. The result sits in the Foundation layer of the Recognition Science mirror, supporting later analytic structure rather than a specific forcing-chain step T0–T8.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.