onRatioOrbit
plain-language theorem explainer
The primitive recognition calculus equips every ratio orbit with the native J-cost J(q) = ((q + q⁻¹)/2) − 1. Character-rigidity and forced-J arguments cite this as the canonical cost object before continuum completion. The body is a pure algebraic combination of orbit add, reciprocal, half, and subtract-one; no analytic step is involved.
Claim. For a ratio orbit $q$, define the PRC J-cost $J(q) := \frac{q + q^{-1}}{2} - 1$ as a ratio-orbit object (add $q$ to its reciprocal, scale by $\tfrac12$, subtract the unit orbit).
background
Ratio orbits are the PRC display of rationals: a signed-orbit numerator over a nonzero distinction-nat denominator (K4.7). They carry total reciprocal (zero maps to zero, as on $\mathbb{Q}$), addition, multiplication, and a fixed half-orbit $1/2$.
The classical Recognition Science cost is $J(x) = (x + x^{-1})/2 - 1$ (equivalently $\cosh(\log x) - 1$), forced unique by the T5 step of the unified forcing chain and the Recognition Composition Law. This definition is the same formula, internalized at the ratio-orbit level rather than on $\mathbb{R}_{>0}$.
The module separates that algebraic object from the later real-analytic uniqueness bridge: the doc-comment states explicitly that uniqueness is not claimed here.
proof idea
Pure definitional construction. Form $q + q^{-1}$, multiply by the half-orbit, then subtract the unit orbit. No lemmas, no tactics; the term is the formula.
why it matters
This is the canonical PRC cost that calibrated characters are forced to match. Downstream, cost-from-character rigidity equates the character-generated cost to this object on calibration points; the doubled-trace and single-prime direction theorems package the same comparison. Gauge-orbit native costs for signed power characters also route through it.
In the continuum layer it is the target of calibrated_character_forces_J and of calibration propagation along cyclic subgroups. Framework-wise it is the ratio-orbit avatar of the T5 J-cost before completion to the real uniqueness theorem. It does not itself close uniqueness; it supplies the rigid reference object those arguments compare against.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.