deriv2_of_logCurvature
plain-language theorem explainer
Unit log curvature forces the second derivative at the origin to equal 1 for any smooth real function normalized at 0 with vanishing first derivative. Cited by the two-premise T5 cost-uniqueness argument that recovers J from the composition law plus curvature calibration. Proof is a one-line uniqueness-of-limits step against the l'Hôpital identification lemma.
Claim. Let $H:\mathbb{R}\to\mathbb{R}$ be $C^\infty$. If $H(0)=1$, $H'(0)=0$, and the log curvature of $H$ equals $1$ (that is, $\lim_{t\to 0,\,t\neq 0} 2(H(t)-1)/t^2 = 1$), then $H''(0)=1$.
background
Module supplies calculus helpers for the T5 cost-uniqueness proof in the Recognition forcing chain. The key calibration predicate is log curvature: $\kappa(H)=\lim_{t\to 0,,t\neq 0} 2(H(t)-1)/t^2$, taken on the punctured neighbourhood of the origin. The puncture is essential; Lean's total division sends the quotient to 0 at $t=0$, so the full-filter reading would force $\kappa=0$ and make the calibrated value $\kappa=1$ unsatisfiable.
Upstream, logCurvature_eq_deriv2 shows that for smooth $H$ with $H(0)=1$ and $H'(0)=0$, the log curvature exists and equals the ordinary second derivative $H''(0)$. That is the l'Hôpital identification that makes unit calibration nonempty rather than vacuous. The present theorem is the matching uniqueness direction: if the curvature is already known to be 1, the second derivative is pinned to 1.
proof idea
One-line term proof. Apply tendsto_nhds_unique to the two Tendsto statements that both target the same punctured-filter quotient $2(H(t)-1)/t^2$: the upstream lemma logCurvature_eq_deriv2 (which produces Tendsto to $H''(0)$ from smoothness, $H(0)=1$, and $H'(0)=0$) and the hypothesis HasLogCurvature H 1 (Tendsto to 1). Uniqueness of nhds limits yields $H''(0)=1$.
why it matters
Feeds directly into composition_logCurvature_forces_jcost, the two-premise cost theorem: composition law plus unit log curvature force $F=J$ on the positives, with normalization, nonnegativity, and continuity as conclusions rather than hypotheses. That result is the streamlined T5 route (J-uniqueness of the Recognition cost $J(x)=(x+x^{-1})/2-1$), cleaner than the older path that assumed those regularity conditions up front. Without the present pin of $H''(0)=1$, the curvature hypothesis would not connect to the Taylor jet used in the d'Alembert/cosh identification of $J$. Landmark: T5 in the Unified Forcing Chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.