tendsto_H_one_of_log_curvature
plain-language theorem explainer
The lemma shows that a real function H with H(0)=1 and logarithmic curvature κ at the origin satisfies lim t→0 H(t)=1. Analysts deriving the d'Alembert continuity theorem for the T5 uniqueness proof cite this result. The argument constructs successive limits for t²/2 and the curvature ratio, then applies the algebraic identity relating H(t)-1 to their product to deduce convergence to 1.
Claim. Let $H : ℝ → ℝ$ satisfy $H(0) = 1$ and $lim_{t→0} 2(H(t)-1)/t² = κ$. Then $lim_{t→0} H(t) = 1$.
background
This module supplies supporting lemmas for the T5 cost uniqueness argument. The function H is the shifted cost defined by H_F(t) = G_F(t) + 1. HasLogCurvature H κ asserts that the second-order behavior near zero obeys the limit of 2(H(t)-1)/t² to κ as t tends to 0.
proof idea
The tactic proof first obtains tendsto of the identity map at 0, then multiplies to get tendsto of t² and t²/2. It multiplies the curvature tendsto by t²/2 to produce a product limit of zero. The sub_one_eq_mul_ratio identity rewrites H(t)-1 exactly as that product, so its limit is zero. Adding the constant 1 recovers the required tendsto of H to 1.
why it matters
This result is invoked by dAlembert_continuous_of_log_curvature to upgrade the functional equation plus log curvature into full continuity of H. It fills a required step in the T5 J-uniqueness chain by guaranteeing continuity at the identity, allowing standard d'Alembert theory to apply. In the Recognition framework this supports passage from the Recognition Composition Law to the cosh-type identity.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.