HasLogCurvature
plain-language theorem explainer
HasLogCurvature encodes the second-order limit condition at the origin for a shifted cost function H. Workers on the T5 J-uniqueness proof cite it to isolate the curvature that selects cosh-type solutions to the d'Alembert equation. The declaration is a direct Filter.Tendsto statement on the normalized second difference quotient.
Claim. A map $H : ℝ → ℝ$ has logarithmic curvature $κ$ when the limit as $t$ approaches 0 of $2(H(t) - 1)/t^2$ equals $κ$.
background
The Cost.FunctionalEquation module supplies lemmas for the T5 cost uniqueness proof. Here H is the shifted cost reparametrization H_F(t) := G_F(t) + 1. Upstream the algebra module defines the shifted cost by H(x) = J(x) + 1 = ½(x + x^{-1}), which converts the Recognition Composition Law into the d'Alembert equation H(xy) + H(x/y) = 2 H(x) H(y).
proof idea
This is a definition. It directly states the required limit via Filter.Tendsto applied to the second difference quotient centered at zero.
why it matters
HasLogCurvature feeds the continuity and cosh-solution theorems for d'Alembert functions (dAlembert_continuous_of_log_curvature, dAlembert_cosh_solution_of_log_curvature). It also supplies the limit form IsCalibratedLimit that links to the normalized IsCalibrated predicate, closing the calibration step inside the T5 J-uniqueness chain. The definition enforces the local curvature that matches the J-cost at the origin.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.
papers checked against this theorem (showing 1 of 1)
-
One log-mean criterion settles four dispersal rules at once
"the asymptotic behaviour—survival or extinction—is governed by the associated log-mean process S_n = Σ log μ_k, where μ_k denotes the expected number of offspring in generation k"