crossDiff_of_crossEq
plain-language theorem explainer
Cross-equal ratio orbits have vanishing cross-difference: the integer numerator of a−b is zero whenever cross-multiplication balances. Anyone proving that the eta unit map is well-defined on delta-rationals cites this. The proof rewrites cross-equality to integer cross-product equality, unfolds the difference, and closes by linear arithmetic.
Claim. If two ratio orbits $a$ and $b$ are cross-equal, meaning $a_{\mathrm{num}}\,b_{\mathrm{den}}=b_{\mathrm{num}}\,a_{\mathrm{den}}$ as integers, then their cross-difference vanishes: $a_{\mathrm{num}}\,b_{\mathrm{den}}-b_{\mathrm{num}}\,a_{\mathrm{den}}=0$.
background
A ratio orbit is the PRC display of a rational: a signed-orbit numerator over a nonzero distinction-nat denominator, with no appeal to Mathlib's $\mathbb{Q}$. Cross-equality is the internal equivalence: two orbits match when the scaled numerators $a_{\mathrm{num}}\cdot b_{\mathrm{den}}$ and $b_{\mathrm{num}}\cdot a_{\mathrm{den}}$ are balanced as signed orbits. The choice-free hub is the integer characterization: cross-equality holds iff the integer cross products agree (only propext and Quot.sound).
The cross-difference is the integer numerator of $a-b$, namely $a_{\mathrm{num}}b_{\mathrm{den}}-b_{\mathrm{num}}a_{\mathrm{den}}$, kept entirely in $\mathbb{Z}$ so the $\mathbb{Q}$ display is never opened. This module builds the eta completion: the unit map sending delta-rationals into regular sequences of integer approximations.
proof idea
Short tactic proof. Rewrite the hypothesis with the choice-free bridge crossEq_iff_toIntCross, which turns cross-equality into equality of the two integer cross products. Unfold crossDiff to expose exactly those products as a difference. Close with omega: equal integers differ by zero.
why it matters
Feeds eta_respects_crossEq, the key well-definedness fact for the unit map: if $q$ and $r$ represent the same delta-rational under cross-equality, then eta q and eta r are equivalent regular sequences. Without vanishing cross-difference on the equivalence class, the sequence construction would depend on the representative. This sits in the Primitive Recognition Calculus foundation layer that builds rationals and their completion from $\delta$-orbits before any continuum structure is assumed; it is bookkeeping for the eta map, not a forcing-chain landmark (T5–T8), but it keeps the rational layer choice-free.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.