isCalibrated_of_isCalibratedLimit
plain-language theorem explainer
The lemma shows that a normalized cost function F whose shifted H_F is twice differentiable with vanishing first derivative at zero has its logarithmic curvature limit equal to the second derivative value implying G''(0)=1. Workers on the T5 J-uniqueness proof in Recognition Science cite this to equate the two calibration formulations. The tactic proof extracts normalization, applies limit uniqueness to fix the second derivative at 1, and transfers derivatives from H back to G via the constant shift.
Claim. Let $F:ℝ→ℝ$ satisfy $F(1)=0$. Suppose $H_F$ is twice continuously differentiable with $(H_F)'(0)=0$ and the logarithmic curvature of $H_F$ at zero equals its second derivative at zero. If the limit form holds, i.e., $lim_{t→0} 2(H_F(t)-1)/t^2=1$, then the derivative form holds: $(G_F)''(0)=1$, where $G_F(t)=F(e^t)$ and $H_F(t)=G_F(t)+1$.
background
This module supplies helper lemmas for the T5 cost uniqueness proof. The cost function F is reparametrized by the log-coordinate map G_F(t)=F(exp t) and the shifted version H_F(t)=G_F(t)+1. IsNormalized requires F(1)=0. HasLogCurvature encodes the limit lim_{t→0} 2(H(t)−1)/t²=κ. IsCalibratedLimit sets κ=1 while IsCalibrated requires the second derivative of G_F at 0 to equal 1.
proof idea
The tactic proof first extracts F(1)=0 from IsNormalized and computes H_F(0)=1. It applies tendsto_nhds_unique to equate the second derivative of H_F at 0 with the limit value 1 from IsCalibratedLimit. Derivatives are transferred from H_F to G_F by noting that H_F differs from G_F by the constant 1, so their first and second derivatives coincide. The final simpa closes the goal for IsCalibrated.
why it matters
This lemma closes the equivalence between limit and derivative forms of calibration inside the T5 uniqueness argument. It feeds the main T5 theorem by allowing either formulation of the calibration hypothesis. In the Recognition framework it supports the forcing of J-uniqueness (T5) via the Recognition Composition Law and the phi-ladder structure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.