dAlembert_cosh_solution_of_log_curvature
plain-language theorem explainer
This theorem shows that a real-valued function H satisfying the d'Alembert equation with H(0)=1, calibrated so its second derivative at zero is 1 via the logarithmic curvature condition, and meeting the listed smoothness and ODE regularity hypotheses, must equal the hyperbolic cosine. It would be cited in the T5 step of Recognition Science to pin down the unique form of the reciprocal cost function. The proof is a one-line wrapper that first extracts continuity from the curvature hypothesis and then applies the core d'Alembert cosh solution.
Claim. Let $H:ℝ→ℝ$ satisfy $H(0)=1$ and the d'Alembert equation $H(t+u)+H(t-u)=2H(t)H(u)$ for all real $t,u$. Assume the logarithmic curvature condition holds with the second derivative of $H$ at the origin equal to 1, together with the smoothness and ODE regularity hypotheses. Then $H(t)=cosh(t)$ for all real $t$.
background
The Cost.FunctionalEquation module supplies lemmas for the T5 cost uniqueness proof. Here H is the shifted cost function defined by H(t)=G(t)+1, where G is the J-cost; this reparametrization converts the Recognition Composition Law into the classical d'Alembert equation. The predicate HasLogCurvature H κ encodes the second-order calibration at the origin via the limit of 2(H(t)-1)/t² approaching κ as t→0; the derivative hypothesis fixes κ=1.
proof idea
The proof is a one-line wrapper. It first invokes dAlembert_continuous_of_log_curvature on the given hypotheses to obtain continuity of H. It then feeds this continuity together with the remaining hypotheses directly into dAlembert_cosh_solution to conclude the identification with cosh.
why it matters
This declaration completes the identification of the cost function with cosh under logarithmic curvature, which is required for the T5 J-uniqueness step in the Recognition Science forcing chain. It relies on the d'Alembert equation that follows from the reciprocal cost definition and supports downstream results on the phi-ladder and mass formulas. The result aligns with the framework landmark that J(x) equals cosh(log x)-1.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.