jq_closed
plain-language theorem explainer
For any nonzero rational t, the J-display equals (t-1)^2/(2t). Cost-ledger and zero-orbit uniqueness arguments cite this closed form constantly. The proof is a three-step algebraic reduction: unfold the definition, clear denominators, and ring-normalize.
Claim. For every nonzero rational $t$, $J(t)=\frac{(t-1)^2}{2t}$, where $J(t)=\frac{t+t^{-1}}{2}-1$.
background
The module builds a structural ledger for the native recognition cost on rationals. The J-display on a rational is the elementary cost
$$J(t)=\frac{t+t^{-1}}{2}-1$$
(defined only for $t\neq 0$). This is the rational specialization of the unique cost functional forced by the Recognition Composition Law and T5 (J-uniqueness): $J(x)=\cosh(\log x)-1$, equivalently $(x+x^{-1})/2-1$.
Working over $\mathbb{Q}$ rather than $\mathbb{R}_{>0}$ lets the ledger stay inside a decidable field, so sign and zero-set facts become pure algebra. The closed form below is the bridge from the symmetric definition to those sign and uniqueness lemmas.
proof idea
Term-mode algebraic identity. Unfold the definition of the J-display, apply field_simp to clear the inverse and common denominators (using $t\neq 0$), then ring to normalize both sides to the same polynomial expression. No external lemmas beyond the field structure of $\mathbb{Q}$.
why it matters
This identity is the workhorse for the three immediate sign/zero facts in the same ledger: nonnegativity on positive rationals, strict negativity on negative rationals, and the characterization that the only zero-cost orbit is the unit ($t=1$). Those facts pin the rational cost landscape that the Primitive Recognition Calculus uses when it certifies minimality of the native cost. In the broader forcing chain this is the rational shadow of T5 J-uniqueness and the RCL identity $J(xy)+J(x/y)=2J(x)J(y)+2J(x)+2J(y)$; the closed form makes the quadratic defect $(t-1)^2$ visible, which is exactly what forces uniqueness of the zero.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.