crossDisp
plain-language theorem explainer
Cross-equivalence of two ratio orbits implies equality of their rational verifier displays. Cost and gauge-orbit arguments cite this constantly when a universal crossEq hypothesis must be turned into a concrete rational identity at a test point. The proof is a one-line application of the forward direction of the cross-multiplication iff.
Claim. If $a$ and $b$ are ratio orbits and $a$ is cross-equivalent to $b$ (cross-multiplication balances the scaled signed numerators against the denominators), then the rational displays agree: $a^{\mathrm{to}\mathbb{Q}} = b^{\mathrm{to}\mathbb{Q}}$.
background
In the Primitive Recognition Calculus, a ratio orbit is an integer numerator (signed orbit) over a nonzero distinction-nat denominator. Its verifier display toRat is the ordinary rational $(n:(\mathbb{Z}))/(d:(\mathbb{N}))$. Internally, equality of ratio orbits is not stated by that display; it is the cross-multiplication relation crossEq: the scaled signed orbits $a.num\cdot b.den$ and $b.num\cdot a.den$ are balanced.
Upstream, K4.10 records that this internal relation is exactly rational equality of displays: crossEq a b if and only if a.toRat = b.toRat. The present lemma is the forward reading of that equivalence. The module sits in the structural ledger for PRC native cost, where characters and candidate costs are compared by cross-equivalence rather than by raw rationals.
proof idea
One-line term proof. Apply the forward (mp) direction of RatioOrbit.crossEq_iff_toRat_eq a b to the given cross-equivalence hypothesis. No further unfolding or arithmetic is needed here; the heavy lifting (balanced signed orbits to integer equality, then to rational equality after nonzero denominator casts) already lives in that iff.
why it matters
This is the standard bridge from internal PRC equality to concrete rational identities used throughout native-cost uniqueness and gauge-orbit classification. Downstream, nondegeneracy and exclusion lemmas apply it at the test point two: charges_at_two_iff_not_signGauge, signedPowerNativeCost_one_not_oddPower, signedPowerNativeCost_one_not_signGauge, and signGaugeNativeCost_not_oddPowerGeneratedNativeCost all open a universal crossEq hypothesis, run this lemma, and obtain a rational contradiction. Inside the structural ledger it feeds character_display (characters respect display equality), the cube/square non-canonicity checks, and the proved uniqueness target PRCStructuralNativeCostUniquenessTarget_proved. It is bookkeeping, but without it every cost-separation argument would re-open the K4.10 arithmetic.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.