crossEq_iff_toRat_eq
plain-language theorem explainer
Cross-multiplication of two ratio orbits is equivalent to equality of their rational verifier displays. Anyone moving between the integer-level PRC ratio calculus and Mathlib $\mathbb{Q}$ cites this bridge. The proof unfolds both sides, reduces scaled numerators via the signed-orbit balance criterion, then closes both directions by field simplification and linear arithmetic over $\mathbb{Q}$.
Claim. Let $a,b$ be ratio orbits (each a signed-orbit numerator over a nonzero distinction-nat denominator). The integer cross-products of $a$ and $b$ agree if and only if their rational verifier displays are equal: $a_{\mathbb{Q}}=b_{\mathbb{Q}}$.
background
A ratio orbit is the PRC display of a rational: a signed orbit as numerator and a nonzero distinction-nat as denominator. Its verifier map sends the pair to the Mathlib rational formed by casting the recovered integer numerator over the recovered natural denominator.
Cross-equality is the integer-level relation that says the two cross-scaled signed orbits are balanced (equivalently, their recovered integers agree). The sibling balance criterion states that two signed orbits are balanced exactly when their integer recoveries coincide; scaling a signed orbit by a natural multiplies that recovery accordingly.
This module sits in the primitive recognition calculus that builds integers and rationals from logic-level orbits, then exposes verifier bridges into Mathlib so cost and character arguments can quote ordinary field arithmetic.
proof idea
Unfold cross-equality and the rational display. Rewrite the balance side with the signed-orbit criterion that balance iff integer recovery agrees, then apply the scaling law for integer recovery on both cross terms.
Both directions are then ordinary rational arithmetic: nonzero denominator casts give the field-simp hypotheses; one direction casts the integer cross identity into $\mathbb{Q}$ and finishes by linarith, the other clears denominators in the rational equality, casts back to $\mathbb{Z}$, and returns the integer cross identity.
why it matters
This is the $\mathbb{Q}$-display bridge labeled K4.10: it lets every later PRC argument that is most naturally stated with cross-equality quote Mathlib rational equality, and conversely.
Downstream it is the rewrite used to discharge reciprocal and zero-calibration obligations for signed-power and sign-gauge native costs, and to move doubled-trace and rational-trace forms of the composition law between orbit syntax and ordinary $\mathbb{Q}$ identities. Those cost factorizations sit on the path from the Recognition Composition Law toward the unique $J$-cost (forcing step T5).
A sibling choice-free integer characterization exists precisely because this bridge routes through Mathlib $\mathbb{Q}$ and therefore classical choice; the present lemma is the convenient display form, not the axiom-light hub.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.