dAlembert_to_ODE_of_contDiff
plain-language theorem explainer
A twice continuously differentiable solution to the d'Alembert functional equation with second derivative calibrated to one at the origin satisfies the ODE H'' = H at every point. Researchers reducing the T5 regularity seam in Recognition Science cite this step to reach the cosh form without extra hypotheses. The proof applies the second-derivative identity lemma at zero, substitutes the calibration, and closes by linear arithmetic.
Claim. Let $H:ℝ→ℝ$ be twice continuously differentiable and obey the d'Alembert equation $H(t+u)+H(t-u)=2H(t)H(u)$ for all real $t,u$. If $H''(0)=1$, then $H''(t)=H(t)$ for every real $t$.
background
The ContDiffReduction module removes an explicit regularity seam for T5 by showing that a C² d'Alembert solution with calibrated second derivative obeys the ODE H''=H. The d'Alembert equation is the functional equation appearing in the signature. The upstream lemma dAlembert_second_deriv_at_zero_of_contDiff states that differentiation of the first-derivative identity at u=0 yields 2H''(t)=2H(t)H''(0) for all t.
proof idea
One-line wrapper that applies dAlembert_second_deriv_at_zero_of_contDiff to obtain the relation 2H''(t)=2H(t)H''(0), rewrites the right-hand side using the given calibration H''(0)=1, and concludes by linarith.
why it matters
The result feeds dAlembert_cosh_solution_of_contDiff, which concludes that C² solutions equal cosh, and the hypothesis bridge dAlembert_to_ODE_hypothesis_of_contDiff. It fills the first advance listed in the module doc-comment: a ContDiff ℝ 2 d'Alembert solution satisfies H''=H. This step removes a central portion of the T5 regularity seam and connects to the J-uniqueness forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.