onRatioOrbit_congr
plain-language theorem explainer
Cross-equivalence of ratio orbits is preserved by the rational J-cost map J(q)=(q+q^{-1})/2-1. Anyone proving PRC character calibration or cost-from-character congruences cites this. The proof is a short rewrite through the toRat display and the closed form of J.
Claim. If two ratio orbits $a$ and $b$ satisfy the cross-multiplication relation $a\sim b$ (i.e. $a_{\mathrm{num}}\cdot b_{\mathrm{den}}$ balances $b_{\mathrm{num}}\cdot a_{\mathrm{den}}$ as signed orbits), then $J(a)\sim J(b)$, where $J(q)=\frac{q+q^{-1}}{2}-1$ is evaluated as a ratio-orbit object.
background
In the Primitive Recognition Calculus, a ratio orbit is an integer numerator over a nonzero orbit denominator: the internal display of a rational. Two such displays are related by cross-equivalence when scaled numerators balance as signed orbits; that relation is exactly rational equality of the verifier displays (crossEq_iff_toRat_eq).
The object onRatioOrbit is PRC's native J-cost on those displays: $J(q)=((q+q^{-1})/2)-1$, built from ratio-orbit add, recip, mul, and sub. Its verifier identity is the ordinary real formula: (onRatioOrbit q).toRat = (q.toRat + q.toRat⁻¹)/2 - 1.
This module develops native uniqueness of that cost from character and doubled-trace hypotheses, staying inside δ-orbit arithmetic rather than analytic uniqueness over ℝ.
proof idea
One short tactic proof. Rewrite the hypothesis and the goal with crossEq_iff_toRat_eq, turning both sides into equality of rational displays. Then rewrite each side with onRatioOrbit_toRat and substitute the hypothesis: equal inputs yield equal J-values, hence the images remain cross-equivalent.
why it matters
This is the basic congruence lemma for the rational J-cost under the internal PRC equivalence. Downstream it is applied directly in absValueCharacter_prime_calibrated (prime-direction calibration of the absolute-value character) and in the family of costFromCharacter_*_congr lemmas (mul, div, reciprocal, normalize). Those feed prime-pair product cost consistency and two-adic axis-twist calibration inside native cost uniqueness.
In the broader RS chain this supports the T5 J-uniqueness story at the discrete ratio-orbit level: J is well-defined on equivalence classes of rationals before any real-analytic bridge. Without this congruence, character-to-cost maps would not descend cleanly along crossEq.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.