crossEq_iff_toIntCross
plain-language theorem explainer
Two ratio orbits are cross-equal exactly when their integer cross-products agree: num(a)·den(b) = num(b)·den(a) in ℤ. Anyone building PRC rationals without Classical.choice cites this as the hub that turns internal balanced-orbit equality into ordinary integer arithmetic. The proof unfolds the definition and rewrites through the balanced↔toInt bridge and the scale-by-Nat display law.
Claim. For ratio orbits $a,b$ (signed-orbit numerator over nonzero distinction-Nat denominator), the internal cross-multiplication relation holds if and only if $a_{\mathrm{num}}^{\mathbb{Z}}\cdot b_{\mathrm{den}}^{\mathbb{N}} = b_{\mathrm{num}}^{\mathbb{Z}}\cdot a_{\mathrm{den}}^{\mathbb{N}}$ in $\mathbb{Z}$.
background
In the Primitive Recognition Calculus, rationals are displayed as RatioOrbit: a signed orbit numerator over a nonzero distinction-Nat denominator. Equivalence of two such displays is not imported from Mathlib ℚ; it is the internal relation that the scaled numerators balance as signed orbits: $a.num$ scaled by $b.den$ balances $b.num$ scaled by $a.den$.
Signed orbits carry a conservative integer display toInt, and balance of two signed orbits is equivalent to equality of those integers (K4.9). Scaling a signed orbit by a distinction-Nat multiplies the integer display by the Nat value of the scale. Together these give a pure-ℤ reading of cross-multiplication.
The module builds integers and rationals from logic-level orbits with only propext and Quot.sound, deliberately avoiding the classical choice that Mathlib's rational field bridge would consume.
proof idea
Term-mode rewrite proof. Unfold the definition of cross-equality to expose balance of the two scaled signed orbits. Rewrite that balance via the K4.9 bridge balanced_iff_toInt_eq, which replaces balance by equality of toInt displays. Apply scaleByNat_toInt on each side so each scaled display becomes the product of the numerator integer with the denominator Nat (cast to ℤ). The goal is then exactly the integer cross-product identity.
why it matters
Doc-comment labels this K4.10: the choice-free integer-level hub through which PRC-rational operations prove respect-of-equivalence. Downstream, crossDiff_of_crossEq and crossEq_of_equiv_eta (Archimedean step for η-completion) route through it; so do antisymmetry and transitivity of the native order leQ on ratio orbits, and the additive structure lemmas that must respect cross-equality (add_respects_cross, add_assoc, add_comm, add_negate).
Without this bridge, every rational congruence argument would either re-expand orbit balance by hand or fall back to the ℚ-display lemma that pulls Classical.choice. It is the purified interface that keeps the rational layer inside {propext, Quot.sound} while still speaking ordinary integer cross-multiplication.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.