jcost_hasLogCurvature_one
plain-language theorem explainer
The shifted canonical cost equals cosh and therefore has unit log-curvature κ=1 on the punctured neighborhood of 0. Anyone invoking the two-premise uniqueness argument (composition law plus unit curvature) needs this non-vacuity witness. The proof equates the H-reparametrization of J to Real.cosh and reads the second derivative at the origin.
Claim. Let $J(x)=\frac{x+x^{-1}}{2}-1$ be the canonical recognition cost and let $H_J$ be its shifted reparametrization $H_J(t)=G_J(t)+1$. Then $H_J$ has unit log-curvature: $\displaystyle\lim_{t\to 0,\,t\neq 0}\frac{2(H_J(t)-1)}{t^2}=1$.
background
Module Cost.FunctionalEquation supplies lemmas for the T5 uniqueness proof: the recognition cost is forced to be $J(x)=\frac{x+x^{-1}}{2}-1$ (equivalently $\cosh(\log x)-1$). The convenience shift $H_F(t)=G_F(t)+1$ turns the Recognition Composition Law into d'Alembert's equation $H(xy)+H(x/y)=2H(x)H(y)$.
Log curvature is the paper's calibration $\kappa(F)=\lim_{t\to 0}2F(e^t)/t^2$, stated here on the punctured filter nhdsWithin 0 {0}ᶜ. The puncture is essential: Lean's total division sends the quotient to 0 at $t=0$, so the full-neighborhood reading forces $\kappa=0$ and makes the calibrated value $\kappa=1$ unsatisfiable for every function. The doc-comment records that the full-filter version silently vacated two results until 2026-07-25.
Upstream, Jcost_G_eq_cosh_sub_one already identifies the $G$-reparametrization of $J$ with $\cosh-1$, so $H_J=\cosh$.
proof idea
First rewrite: from Jcost_G_eq_cosh_sub_one and the definition $H=G+1$, a pointwise funext plus linarith yields $H\circ J=\mathrm{Real.cosh}$.
Next compute the jet of cosh at 0: Real.deriv_cosh and sinh_zero give $\mathrm{deriv},\cosh,0=0$; a second differentiation with deriv_sinh and cosh_zero gives $\mathrm{deriv}^2\cosh,0=1$.
Apply the general bridge logCurvature_eq_deriv2 (contDiff cosh, value 1 at 0, first derivative 0) to conclude that cosh has log-curvature equal to its second derivative at 0, hence equal to 1. Transport along the equality $H\circ J=\cosh$.
why it matters
T5 in the forcing chain asserts J-uniqueness. The two-premise cost theorem (composition law + unit log curvature) concludes $F=J$ on the positives, with normalization, nonnegativity, and continuity as conclusions rather than hypotheses; compare law_of_logic_forces_jcost, which assumes those regularity conditions. This lemma is the non-vacuity witness that the calibrated value $\kappa=1$ is attained by the canonical cost, so the curvature hypothesis is not empty.
Without it the uniqueness argument would rest on a regularity condition no model satisfies (the lesson of the retired full-filter reading). It sits squarely in the Cost domain supporting T5 and the Recognition Composition Law identity that becomes d'Alembert under the $H$-shift.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.