dAlembert_second_deriv_at_zero_of_contDiff
plain-language theorem explainer
Any twice continuously differentiable real function satisfying the d'Alembert functional equation has its second derivative at arbitrary t proportional to the function value at t, scaled by the second derivative at zero. Analysts reducing regularity assumptions in the Recognition Composition Law to reach the associated ODE would cite this step. The proof differentiates the first-derivative identity at the origin, applies chain-rule HasDerivAt statements for the linear shifts, and simplifies the resulting equality with linear arithmetic.
Claim. Let $H : ℝ → ℝ$ be twice continuously differentiable and satisfy the d'Alembert equation $H(t + u) + H(t - u) = 2 H(t) H(u)$ for all real $t, u$. Then $2 H''(t) = 2 H(t) H''(0)$ for all real $t$.
background
The ContDiffReduction module removes a central portion of the explicit T5 regularity seam. Its goal is to show that any ContDiff ℝ 2 solution to the d'Alembert equation satisfies the ODE H'' = H, so that the canonical reciprocal cost follows from normalization, composition, and calibration alone. The shifted cost is defined by H(x) = J(x) + 1, where J satisfies the Recognition Composition Law; under this shift the law becomes the additive d'Alembert equation shown in the signature.
proof idea
The tactic proof first applies dAlembert_first_deriv_of_contDiff to obtain the identity (fun u => deriv Hf (t + u) - deriv Hf (t - u)) = ((fun _ => 2 * Hf t) * deriv Hf). It then builds HasDerivAt statements at u = 0 for both sides: the left via hasDerivAt_deriv_of_contDiffTwo composed with the linear maps t + u and t - u, the right via the constant 2 * Hf t multiplied by the derivative at zero. Equating the derivatives at zero via congrArg and rewriting with .deriv yields the claim after linarith.
why it matters
This supplies the differentiation step that feeds directly into dAlembert_to_ODE_of_contDiff, whose doc-comment states that a C² d'Alembert solution with calibrated second derivative satisfies H'' = H. In the Recognition framework it closes the explicit regularity seam for T5 J-uniqueness, allowing the canonical reciprocal cost to be recovered from the Composition Law, normalization, and the calibration H''(0) = 1 alone.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.