jq_one
plain-language theorem explainer
The rational J-display vanishes at the unit: J(1) = 0. Anyone normalizing native cost on ratio orbits or checking the zero-cost fixed point of reciprocal will cite this. The proof is a one-line numeric unfold of the closed form (t + t^{-1})/2 - 1.
Claim. The rational J-display $J_{\mathbb{Q}}(t) = (t + t^{-1})/2 - 1$ satisfies $J_{\mathbb{Q}}(1) = 0$.
background
In the Primitive Recognition Calculus native-cost ledger, the structural cost on rationals is the J-display
$$J_{\mathbb{Q}}(t) := \frac{t + t^{-1}}{2} - 1.$$
This is the same functional form forced uniquely (up to gauge) by the Recognition Composition Law and the T5 uniqueness step of the forcing chain: $J(x) = (x + x^{-1})/2 - 1$, equivalently $\cosh(\log x) - 1$ on positives. The ledger works over $\mathbb{Q}$ so that ratio-orbit costs stay exact before any real completion.
The unit $t = 1$ is the self-reciprocal point of the multiplicative group. Evaluating $J$ there is the base case for every later statement that zero cost means the orbit is the unit.
proof idea
One-line wrapper: unfold the definition of the rational J-display and discharge the resulting rational arithmetic by norm_num. No lemmas beyond the definition are required.
why it matters
This is the elementary normalization that the rest of the structural ledger leans on. Downstream, native_recip_fixed_iff_cost_zero uses it to prove that on the positive cone the reciprocal fixes exactly the zero-cost orbit: the unit is the only thing that costs nothing and the only self-reciprocal positive orbit. The degenerate-gauge result trivial_of_two_eq_one (the sign character, $c = 0$ member of the power family) likewise needs the unit evaluation when anchoring collapses the whole cost.
In the broader framework this is the rational shadow of T5 J-uniqueness: once $J(1) = 0$ is locked, non-negativity, the closed form on ratio orbits, and the identification of zero cost with the unit all become available without leaving $\mathbb{Q}$.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.