crossEq
plain-language theorem explainer
Cross-multiplication equality on ratio orbits: two displays match when the numerator of each, scaled by the other's denominator, balances as signed orbits. Cost and gauge-orbit authors cite it as the internal PRC stand-in for rational equality. The body is a one-line reduction to signed-orbit balance after denominator scaling.
Claim. For ratio orbits $a=(n_a,d_a)$ and $b=(n_b,d_b)$ (signed-orbit numerators over nonzero distinction-nat denominators), cross-equality holds when the signed orbit $n_a$ scaled by $d_b$ balances $n_b$ scaled by $d_a$, i.e. their positive and negative orbit lengths satisfy the integer balance identity after scaling.
background
In the Primitive Recognition Calculus integer/rational layer, integers are carried as signed orbits: a pair of distinction-nat lengths with intended meaning $\mathrm{pos}-\mathrm{neg}$. Two signed orbits are balanced when $a.pos+b.neg=b.pos+a.neg$ (K4.9), the internal integer equality on $\delta$-orbit positions.
A ratio orbit (K4.7) packages a signed-orbit numerator over a nonzero distinction-nat denominator. Scaling a signed orbit by a distinction nat multiplies both legs: $\mathrm{scaleByNat},z,d$ has legs $z.pos\cdot d$ and $z.neg\cdot d$. Cross-equality is the PRC analogue of $n_a/d_a=n_b/d_b$ via $n_a d_b=n_b d_a$, stated entirely inside that language.
The module builds verifier displays for rationals without leaving orbit arithmetic; ordinary $\mathbb{Q}$ equality is recovered only after a separate display map.
proof idea
Definitional one-liner: apply signed-orbit balance to the pair obtained by scaling each numerator by the other denominator. No tactics, no lemmas beyond the constructors of SignedOrbit.balanced and scaleByNat.
why it matters
This is the equality relation used by the gauge-orbit cost classification. Downstream theorems such as degenerate_is_signGauge, nontrivial_is_signedPower, and charges_at_two_iff_not_signGauge state that a structural native cost $F$ agrees with the sign gauge or a signed-power cost by asserting $\mathrm{crossEq},(F,q),(\ldots,q)$ for every ratio orbit $q$.
The family propositions GaugeOrbitIsSignedPowerFamily and the still-open GaugeOrbitIsSignOrOddPowerFamily are quantified over universal cross-equality to those model costs. Without an internal rational relation, the classification could not stay inside PRC displays. Landmark link: native cost uniqueness and the J-cost forcing chain need a well-defined equality on ratio displays before comparing candidate costs.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.