onRatioOrbit_crossEq
plain-language theorem explainer
If two ratio orbits represent the same rational, their canonical PRC J-costs also represent the same rational. Character-rigidity arguments cite this to move cost equality across the internal cross-multiplication relation rather than through real embeddings. The proof rewrites cross-equivalence as rational equality and applies the closed-form display of the orbit J-cost twice.
Claim. Let $a,b$ be ratio orbits. If $a$ and $b$ are cross-equivalent (equivalently $a$ and $b$ display the same rational), then the canonical PRC costs $J(a)=\frac{a+a^{-1}}{2}-1$ and $J(b)=\frac{b+b^{-1}}{2}-1$, computed as ratio-orbit objects, are likewise cross-equivalent.
background
In the Primitive Recognition Calculus, rationals are carried as RatioOrbit objects: a signed-orbit numerator over a nonzero distinction-orbit denominator. Two such displays are related by cross-equivalence when the cross-multiplied signed orbits balance, which is the internal stand-in for ordinary rational equality (K4.10). The bridge lemma states that cross-equivalence holds if and only if the verifier rationals agree.
The canonical PRC cost on a ratio orbit is the orbit-level J-cost $J(q)=((q+q^{-1})/2)-1$, built from orbit addition, reciprocal, scaling by one-half, and subtraction of the unit orbit. Its verifier display is exactly the familiar real formula $(q+q^{-1})/2-1$. This module sits in the continuum character-rigidity layer: calibrated multiplicative characters on ratio orbits are forced to reproduce that same cost.
proof idea
Short rewrite proof. First replace the hypothesis and the goal by the iff that identifies cross-equivalence with equality of toRat displays. Then rewrite both sides of the goal with the closed form (onRatioOrbit q).toRat = (q.toRat + q.toRat⁻¹)/2 - 1. The two displays become identical functions of equal rationals, so the goal is the hypothesis.
why it matters
This is the congruence lemma that lets cost comparisons stay inside the PRC ratio-orbit language. Downstream, costFromCharacter_rigid applies it once: if a calibrated character agrees with the identity at a point $p$, the character-generated cost is cross-equivalent to the canonical orbit J-cost at $p$. That step is the local forcing that a calibrated character cannot invent a second cost functional on calibration points.
In the broader Recognition chain this protects T5-style J-uniqueness at the discrete rational layer before continuum uniqueness is invoked: the Recognition Composition Law's cost $J(x)=\cosh(\log x)-1$ is already the unique orbit object compatible with cross-equivalence. Without this lemma, character rigidity would have to exit to $\mathbb{Q}$ or $\mathbb{R}$ at every comparison.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.