logCurvature_eq_deriv2
plain-language theorem explainer
For C^∞ functions with F(0)=1 and F'(0)=0, the log-curvature limit equals F''(0). Cited in the T5 cost-uniqueness chain to equate the paper's κ-calibration with ordinary second derivative data. Proof is a punctured-filter l'Hôpital argument on the quotient 2(F(t)-1)/t².
Claim. Let $F:\mathbb{R}\to\mathbb{R}$ be $C^\infty$ with $F(0)=1$ and $F'(0)=0$. Then the log curvature of $F$ exists and equals $F''(0)$: $\lim_{t\to 0,\,t\neq 0} 2(F(t)-1)/t^2 = F''(0)$.
background
The module supplies calculus lemmas for the T5 cost-uniqueness proof in the forcing chain. T5 identifies the unique cost functional $J(x)=(x+x^{-1})/2-1$ (equivalently $\cosh(\log x)-1$) satisfying the Recognition Composition Law.
Log curvature is the paper's calibration invariant $\kappa(F)=\lim_{t\to 0} 2(F(t)-1)/t^2$, stated on the punctured filter $\mathrm{nhdsWithin},0,{0}^c$. The puncture is essential: Lean's total division sends the quotient to $0$ at $t=0$, so the full-neighbourhood reading forces $\kappa=0$ and makes the unit calibration empty.
The hypotheses $F(0)=1$ and $F'(0)=0$ match the even, unit-normalized profile of the composed cost $H\circ J$ after the change of variables $t=\log x$. Smoothness supplies the second derivative needed to identify $\kappa$ with $F''(0)$.
proof idea
Downgrade $C^\infty$ to $C^2$ so that $\mathrm{deriv},F$ is differentiable. The second derivative at $0$ is then a genuine derivative of the first derivative, hence equals the slope limit $\mathrm{deriv},F(t)/t$ on the punctured neighbourhood (using $F'(0)=0$).
Apply l'Hôpital on the punctured filter: numerator $2(F(t)-1)\to 0$ by continuity and $F(0)=1$; denominator $t^2\to 0$; both are differentiable off zero with derivatives $2F'(t)$ and $2t$, and the derivative quotient simplifies to $F'(t)/t$, which tends to $F''(0)$. The conclusion is exactly $\mathrm{HasLogCurvature},F,F''(0)$.
why it matters
This is the l'Hôpital bridge that makes the corrected (punctured) calibration satisfiable rather than empty. Downstream, deriv2_of_logCurvature inverts it: unit log curvature forces $F''(0)=1$. The non-vacuity witness jcost_hasLogCurvature_one then shows the canonical cost $H\circ J=\cosh$ meets $\kappa=1$.
Together these close the calibration step inside T5 J-uniqueness. Without the punctured-filter reading and this identification, the unit-curvature hypothesis would be uninhabited and the uniqueness argument would not attach to any concrete cost. The result is local real analysis; the RS content is that it legitimates the paper's $\kappa=1$ normalisation for $J$.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.