crossDiff_swap
plain-language theorem explainer
Antisymmetry of the integer cross-difference on rational orbits: swapping the two arguments negates the value. Anyone proving symmetry of orbit equivalence or building an order from cross-differences cites this. The proof unfolds the bilinear definition and closes by ring on integers.
Claim. For rational orbits $a$ and $b$ (integer numerator over nonzero orbit denominator), the cross-difference satisfies $\mathrm{cd}(b,a)=-\mathrm{cd}(a,b)$, where $\mathrm{cd}(a,b)=a_{\mathrm{num}}b_{\mathrm{den}}-b_{\mathrm{num}}a_{\mathrm{den}}$ is the integer numerator of $a-b$.
background
A ratio orbit is the primitive display of a rational: a signed-orbit numerator over a nonzero distinction-nat denominator, kept free of a $\mathbb{Q}$ type. The cross-difference of two such orbits is the pure integer $a.num,b.den-b.num,a.den$, i.e. the numerator of $a-b$ after clearing denominators. It is the comparison primitive used throughout the eta-completion layer.
This module (EtaCompletionM0a) builds a choice-free Cauchy-style completion for regular sequences of ratio orbits. Cross-difference is the signed distance that later feeds absolute-value bounds, triangle identities, and the equivalence relation on regular sequences. The next sibling identity records the three-point form that underwrites the triangle inequality after clearing denominators.
proof idea
One-line algebraic proof. Unfold the definition of cross-difference on both sides; the goal becomes the integer identity
$(b.num,a.den-a.num,b.den)=-(a.num,b.den-b.num,a.den)$.
The ring tactic discharges it immediately. No lemmas beyond the definition are required.
why it matters
Feeds equiv_symm in the same module: symmetry of sequence equivalence only needs that the cross-difference flips sign, so absolute value and the denominator product are unchanged (choice-free). That symmetry is part of showing the eta-regular equivalence is an equivalence relation on regular sequences, which is the M0a step toward a completed cost calculus on orbits.
In the broader Primitive Recognition Calculus, cross-difference is the integer stand-in for rational subtraction; antisymmetry is the first algebraic sanity check before the three-point identity and triangle inequality. It sits upstream of any order or metric structure built from the cost on ratio orbits, and is independent of the later J-cost / forcing-chain material (T5–T8).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.