jq_eq_zero
plain-language theorem explainer
On nonzero rationals, the native J-display vanishes only at the unit: J(t)=0 forces t=1. Anyone working the PRC native-cost ledger or reciprocal-fixed orbits cites this uniqueness. The proof rewrites J via its closed form (t-1)^2/(2t) and splits the zero-quotient cases.
Claim. For every nonzero rational $t$, if $J(t)=0$ where $J(t)=(t+t^{-1})/2-1$, then $t=1$. Equivalently, the only zero-cost rational orbit is the unit.
background
In the Primitive Recognition Calculus native-cost ledger, the J-display on a rational is the standard RS cost $J(t)=(t+t^{-1})/2-1$ (also written $\cosh(\log t)-1$). It measures the cost of a ratio orbit relative to the unit.
The closed algebraic form $J(t)=(t-1)^2/(2t)$ for $t\neq 0$ is already proved in-module; it makes the zero set transparent. The same $J$ is the unique continuous solution of the Recognition Composition Law forced at T5 of the Unified Forcing Chain.
Locally the ledger tracks structural identities of this cost on $\mathbb{Q}^\times$ before lifting to ratio orbits and gauge characters. Zero cost is the flat, defect-free point: the unit orbit.
proof idea
Rewrite the hypothesis $J(t)=0$ with the closed form, obtaining $(t-1)^2/(2t)=0$. Split by the rational zero-quotient criterion: either the numerator vanishes or the denominator does.
If $(t-1)^2=0$, then $t-1=0$ by the square-zero lemma (exponent $2\neq 0$), so $t=1$ by linear arithmetic. If $2t=0$, then $t=0$, contradicting the standing nonzero hypothesis. That exhausts the cases.
why it matters
This is the rational kernel of the slogan "the unit is the only zero-cost orbit." Downstream, native_recip_fixed_iff_cost_zero uses it to equate reciprocal-fixed positive orbits with zero native cost: only the unit is self-reciprocal and free. The degenerate gauge collapse trivial_of_two_eq_one and the separation of the sign character from odd-power generated costs also lean on zero-cost uniqueness.
In the forcing chain this is the discrete shadow of T5 J-uniqueness: $J$ vanishes only at $1$, so the cost landscape has a single global minimum. That minimum anchors the phi-ladder yardstick, the Berry threshold, and the defect-to-curvature dictionary (zero defect density means flat space).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.