dAlembert_to_ODE_hypothesis_of_contDiff
Any twice continuously differentiable function satisfying the d'Alembert equation with second derivative calibrated to one at zero obeys the ODE H'' = H. Workers on the T5 J-uniqueness step cite this result to drop explicit regularity hypotheses from the legacy derivation. The argument is a one-line wrapper that unpacks the hypothesis premises and applies the direct ContDiff-to-ODE theorem.
claimIf $H : ℝ → ℝ$ is twice continuously differentiable, then the following holds: whenever $H(0) = 1$, $H$ is continuous, $H(t+u) + H(t-u) = 2 H(t) H(u)$ for all real $t,u$, and the second derivative of $H$ at zero equals 1, it follows that the second derivative of $H$ at every $t$ equals $H(t)$.
background
The d'Alembert_to_ODE_hypothesis is the proposition that a function satisfying normalization at zero, continuity, the d'Alembert functional equation, and second-derivative calibration at zero must obey the ODE H'' = H. Its companion theorem dAlembert_to_ODE_of_contDiff proves the ODE directly from ContDiff ℝ 2 together with the functional equation and the calibration H''(0) = 1. The module removes a central portion of the explicit T5 regularity seam by showing that C² smoothness plus the functional equation suffice for the ODE conclusion.
proof idea
The proof introduces the four premises of the d'Alembert_to_ODE_hypothesis and invokes dAlembert_to_ODE_of_contDiff on Hf, the d'Alembert equation, the ContDiff ℝ 2 assumption, and the second-derivative calibration at zero.
why it matters in Recognition Science
This declaration closes part of the regularity gap in the T5 J-uniqueness chain by bridging the legacy hypothesis to the ContDiff surface. It supports the claim that the canonical reciprocal cost follows from normalization, composition, and calibration alone. The result sits inside the ContDiff reduction for T5 and removes explicit smoothness assumptions from the derivation of the ODE from the composition law.
scope and limits
- Does not establish the d'Alembert equation itself from the composition law.
- Does not prove existence or uniqueness of solutions without the calibration H''(0) = 1.
- Does not address higher-order smoothness or analytic continuation.
- Does not connect the ODE directly to the phi-ladder or mass formulas.
formal statement (Lean)
132theorem dAlembert_to_ODE_hypothesis_of_contDiff
133 (Hf : ℝ → ℝ) (h_diff : ContDiff ℝ 2 Hf) :
134 dAlembert_to_ODE_hypothesis Hf := by
proof body
Term-mode proof.
135 intro _ _ h_dAlembert h_deriv2_zero
136 exact dAlembert_to_ODE_of_contDiff Hf h_dAlembert h_diff h_deriv2_zero
137
138/-- A normalized composition-law cost is automatically reciprocal. -/