jq_zero
plain-language theorem explainer
The rational J-display equals -1 at the origin. Cost-ledger simplifications and character identities on Q cite this boundary value. Proof is a one-line numerical discharge of the definition under the field convention that zero inverse is zero.
Claim. The rational J-display satisfies $J(0)=-1$, where $J(t)=\frac{t+t^{-1}}{2}-1$ on $\mathbb{Q}$ (with the field convention $0^{-1}=0$).
background
In the Primitive Recognition Calculus native-cost ledger, the J-display on rationals is the specialization $J_q(t)=(t+t^{-1})/2-1$. This is the same algebraic shape as the unique cost forced by T5 of the Unified Forcing Chain (and by the Recognition Composition Law): $J(x)=(x+x^{-1})/2-1$, equivalently $\cosh(\log x)-1$ on the positive reals.
On a field, the inverse of zero is defined to be zero. Substituting $t=0$ therefore collapses the expression to a constant rather than leaving a pole. Sibling lemmas in the same module record the other elementary evaluations and sign properties of this display (value at one, nonnegativity, closed forms on ratio orbits).
proof idea
One-line wrapper. Unfold the definition of the rational J-display and run norm_num. With $0^{-1}=0$ the arithmetic is $(0+0)/2-1=-1$. Marked @[simp] so downstream rewrites fire automatically.
why it matters
Gives the origin evaluation of the rational J-display inside the PRC native-cost structural ledger. The J-cost is the T5 landmark of the forcing chain; having its rational special case fully reduced at singular points (under field conventions) keeps cost-minimality certificates and character identities free of ad-hoc case splits. The dependency graph currently lists no downstream consumers, so the lemma functions as local simp infrastructure for the ledger rather than a cited step in a larger theorem.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.