crossDiff
plain-language theorem explainer
The cross-difference of two rational orbits is the integer numerator of their difference: num(a)·den(b) − num(b)·den(a), computed entirely in ℤ. Anyone working on the η-completion or regular-sequence equality cites it as the primitive comparison measure. The body is a one-line arithmetic expression using the signed-orbit and distinction-nat displays.
Claim. For rational orbits $a=(n_a/d_a)$ and $b=(n_b/d_b)$ (integer numerator over nonzero orbit denominator), define the cross-difference $\mathrm{crossDiff}(a,b) := n_a\,d_b - n_b\,d_a \in \mathbb{Z}$. This is the integer numerator of $a-b$ without constructing a rational.
background
A RatioOrbit is the K4.7 display of a rational: a signed orbit numerator over a nonzero distinction-nat denominator. Signed orbits recover ordinary integers via toInt (positive count minus negative count); distinction nats recover ordinary naturals via toNat (iteration count from the identity).
The module builds the η-completion of the rationals inside the Primitive Recognition Calculus, working only with integer arithmetic. Direct subtraction in ℚ is avoided; instead one compares two displays by the integer that would be the numerator of their difference after clearing denominators.
Upstream, RatioOrbit and the two recovery maps (SignedOrbit.toInt, orbit toNat) supply the raw integer data. The cross-difference is the pure-ℤ stand-in for $a-b$.
proof idea
Pure definition: cast the two numerators to ℤ via signed-orbit toInt, cast the two denominators to ℤ via toNat, and form the bilinear expression $n_a d_b - n_b d_a$. No lemmas or tactics; the body is that single arithmetic term.
why it matters
This is the atomic comparison primitive for the entire EtaCompletionM0a development. Downstream it feeds: vanishing on equals (crossDiff_self, crossDiff_of_crossEq), antisymmetry (crossDiff_swap), and the three-point identity that clears denominators in $(a-c)=(a-b)+(b-c)$ (crossDiff_triangle_id), the algebraic backbone of the triangle inequality on regular sequences.
It also appears inside the working equality equiv on regular sequences (pointwise cross-difference eventually smaller than every $1/(k+1)$) and in the Archimedean step crossEq_of_equiv_eta that recovers ordinary cross-equality of constant sequences from sequence equivalence. Without a choice-free integer numerator for $a-b$, the η-regular completion cannot stay inside the logic-derived arithmetic of the foundation layer.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.