dAlembert_cosh_solution_of_contDiff
plain-language theorem explainer
A twice continuously differentiable real function satisfying the d'Alembert equation with f(0)=1 and f''(0)=1 equals cosh. Recognition Science researchers working on T5 uniqueness cite this to close the C² regularity seam. The term proof reduces the functional equation to the ODE f''=f via differentiation lemmas then invokes the cosh uniqueness theorem.
Claim. Let $f : ℝ → ℝ$ be twice continuously differentiable. If $f(0)=1$, $f(t+u)+f(t-u)=2f(t)f(u)$ for all real $t,u$, and the second derivative of $f$ at 0 equals 1, then $f(t)=cosh(t)$ for all real $t$.
background
The shifted cost is defined by H(x) = J(x) + 1, under which the Recognition Composition Law becomes the d'Alembert equation H(xy) + H(x/y) = 2 H(x) H(y). This module reduces the explicit T5 regularity seam by showing that any ContDiff ℝ 2 solution of the d'Alembert equation satisfies the ODE H'' = H. Upstream lemmas include contDiffTwo_differentiable (which extracts differentiability from C²) and dAlembert_to_ODE_of_contDiff (which converts the functional equation into the ODE under the given calibration).
proof idea
The term proof chains four lemmas: dAlembert_to_ODE_of_contDiff produces the ODE ∀t, (deriv (deriv Hf)) t = Hf t; dAlembert_even yields evenness; contDiffTwo_differentiable plus even_deriv_at_zero gives deriv Hf 0 = 0; ode_cosh_uniqueness_contdiff then concludes Hf t = cosh t.
why it matters
This theorem supplies the cosh identification step inside washburn_uniqueness_of_contDiff, which states that normalization, the composition law, calibration, and C² regularity of H = G + 1 already force the canonical reciprocal cost. It directly supports the sharpened T5 surface in the forcing chain (T5 J-uniqueness) by deriving reciprocity rather than assuming it. The result removes one explicit regularity hypothesis from the T5 closure argument.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.