dAlembert_cosh_solution_of_contDiff
plain-language theorem explainer
A twice continuously differentiable solution to the d'Alembert equation with Hf(0)=1 and second derivative 1 at zero equals the hyperbolic cosine. Researchers sharpening the T5 uniqueness surface in Recognition Science cite this to show that C² regularity plus the composition law pins the cost function without assuming reciprocity. The term-mode proof reduces the functional equation to the ODE f''=f, establishes evenness and vanishing first derivative at zero, then invokes the ODE uniqueness lemma.
Claim. Let $H_f : ℝ → ℝ$ satisfy $H_f(0)=1$, the d'Alembert equation $H_f(t+u)+H_f(t-u)=2 H_f(t) H_f(u)$ for all real $t,u$, be twice continuously differentiable, and obey $(H_f'')'(0)=1$. Then $H_f(t)=cosh(t)$ for all real $t$.
background
In Recognition Science the shifted cost is $H(x)=J(x)+1$, where $J$ obeys the Recognition Composition Law. Under this shift the RCL becomes the d'Alembert equation $H(xy)+H(x/y)=2 H(x) H(y)$. The module ContDiffReduction shows that $C^2$ regularity on solutions of this equation converts the functional equation into the ODE $H''=H$ (see dAlembert_to_ODE_of_contDiff).
proof idea
The term proof first calls dAlembert_to_ODE_of_contDiff to obtain the pointwise ODE deriv(deriv Hf)t = Hf t. It then applies dAlembert_even to obtain that Hf is even, uses contDiffTwo_differentiable to get differentiability at zero, invokes even_deriv_at_zero to conclude deriv Hf 0 = 0, and finishes with a direct appeal to ode_cosh_uniqueness_contdiff.
why it matters
This theorem supplies the cosh uniqueness step required by washburn_uniqueness_of_contDiff, which assembles normalization, the composition law, calibration and C² regularity into the sharpened T5 surface. The module doc-comment states that these ingredients already force the canonical reciprocal cost; the result therefore closes one seam in the T5 J-uniqueness forcing chain without extra hypotheses.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.