dAlembert_to_ODE_hypothesis_of_contDiff
plain-language theorem explainer
If a map from the reals to the reals is twice continuously differentiable then the d'Alembert functional equation together with normalization at zero implies the ODE H'' = H. Workers on the T5 J-uniqueness step cite the result to drop an explicit smoothness hypothesis from the legacy derivation. The argument is a one-line wrapper that invokes the stronger contDiff derivation lemma.
Claim. Let $H : ℝ → ℝ$ be twice continuously differentiable. Then $H$ satisfies the d'Alembert-to-ODE hypothesis: whenever $H(0)=1$, $H$ is continuous, $H(t+u)+H(t-u)=2H(t)H(u)$ for all real $t,u$, and the second derivative of $H$ at zero equals one, the second derivative equals $H$ at every point.
background
The module ContDiffReduction removes an explicit regularity seam from the T5 step. The legacy predicate dAlembert_to_ODE_hypothesis (defined in FunctionalEquation) packages the implication: if a function satisfies the d'Alembert equation, is continuous, and has second derivative one at zero, then it obeys the ODE H''=H. The stronger sibling theorem dAlembert_to_ODE_of_contDiff assumes the d'Alembert equation, ContDiff ℝ 2, and the calibration deriv(deriv Hf) 0 = 1, then concludes the ODE everywhere. Upstream, reciprocal is the automorphism that inverts positive ratios, while cost extracts the derived cost from a multiplicative recognizer.
proof idea
One-line wrapper that applies dAlembert_to_ODE_of_contDiff. The tactic intro discharges the four antecedents of the hypothesis predicate and hands them directly to the contDiff derivation lemma together with the given ContDiff assumption.
why it matters
The declaration closes part of the regularity reduction for T5 J-uniqueness in the forcing chain. It shows that, once ContDiff ℝ 2 is granted, the canonical reciprocal cost follows from normalization, the Recognition Composition Law, and calibration alone. No downstream uses are recorded yet; the result therefore sits as an internal bridge inside the ContDiffReduction module.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.