jq_onRatioOrbit
plain-language theorem explainer
The rational display of the native J-cost on a ratio orbit equals the closed form (t + t^{-1})/2 - 1 at the orbit's rational value. Structural-ledger and gauge-orbit cost proofs cite this as the simp bridge between orbit algebra and the rational J display. Proof is a one-line re-export of the existing orbit-to-rational transport.
Claim. For every ratio orbit $q$, the rational value of the orbit-level $J$-cost of $q$ equals $(t + t^{-1})/2 - 1$ evaluated at $t$ equal to the rational display of $q$.
background
A ratio orbit is an integer numerator over a nonzero distinction-nat denominator (K4.7). Its verifier display toRat recovers an ordinary rational by integer division; the internal characterization is cross-multiplication.
The PRC native cost on a ratio orbit is the orbit-algebra object $J(q) = ((q + q^{-1})/2) - 1$. Separately, the rational J display is the same formula written on $\mathbb{Q}$: $(t + t^{-1})/2 - 1$. Upstream, the transport lemma already proves that converting the orbit-level construction to a rational recovers exactly that closed form (by unfolding add, recip, mul, sub, half, and one, then ringing).
This module collects structural ledger identities for that native cost, aimed at uniqueness of the canonical cost among gauge-related candidates.
proof idea
One-line wrapper. The claim is the upstream transport lemma restated with the rational J display on the right-hand side, so the proof is just an application of that transport. The @[simp] attribute lets later ledger rewrites flip between orbit-level cost and the rational formula without re-expanding the orbit algebra.
why it matters
Workhorse simp for the structural native-cost ledger. Downstream uses include reciprocal symmetry of cost, the positive-cone fact that the reciprocal fixes exactly the zero-cost orbit (unit only), power- and odd-power-generated cost displays (showing the canonical cost is the $k=0$ gauge member), and the Round 5 terminal that the structural ledger forces the canonical cost. It also feeds signed-power native-cost transport in the gauge-orbit layer.
In the Recognition forcing chain this is the rational skeleton of T5 J-uniqueness, $J(x)=(x+x^{-1})/2-1$, before the real-analytic uniqueness bridge. Without it every ledger identity would re-expand orbit operations by hand.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.