crossDiff_self
plain-language theorem explainer
The cross-difference of any rational orbit with itself is the integer zero. Anyone building Cauchy-style equivalence or regularity for sequences of RatioOrbit values cites this identity. The proof unfolds the bilinear definition and closes by integer arithmetic (omega).
Claim. For every rational orbit $a$ (integer numerator over a nonzero orbit denominator), the cross-difference of $a$ with itself vanishes: $a_{\mathrm{num}}\,a_{\mathrm{den}} - a_{\mathrm{num}}\,a_{\mathrm{den}} = 0$ in $\mathbb{Z}$.
background
In the primitive recognition calculus, rationals are carried as RatioOrbit: a signed-orbit numerator over a nonzero distinction-nat denominator, avoiding a direct $\mathbb{Q}$ display. The local module builds an $\eta$-style completion of these orbits via regular sequences and an equivalence relation.
The cross-difference of two orbits $a,b$ is the integer numerator of the formal difference $a-b$, namely $a.num\cdot b.den - b.num\cdot a.den$. It is the native comparison primitive used later to state regularity bounds and pairwise equivalence of sequences without leaving the integer layer.
Self-vanishing of that bilinear form is the base algebraic fact needed before any Cauchy or reflexivity argument can start.
proof idea
One-line tactic proof: unfold the definition of cross-difference, obtaining $a.num\cdot a.den - a.num\cdot a.den$, then discharge the integer identity by omega. No external lemmas are required beyond the definition itself.
why it matters
This identity is the algebraic seed for reflexivity of sequence equivalence and for well-formedness of the constant embedding $\eta$. Downstream, equiv_refl rewrites with it (and Int.natAbs_zero) to show every regular sequence is equivalent to itself; eta_regular uses the same rewrite to prove the constant sequence at a fixed orbit satisfies the regularity inequality.
In the broader Recognition stack this sits in the foundation layer that prepares discrete rational displays before cost and forcing arguments (J-uniqueness, $\varphi$-ladder) attach. It does not itself touch T5–T8; it only clears the integer arithmetic needed so those later layers can treat rational orbits as a completed ordered field-like object.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.