dAlembert_first_deriv_of_contDiff
plain-language theorem explainer
A twice continuously differentiable solution to the d'Alembert functional equation satisfies the once-differentiated identity in the second variable. Researchers closing the T5 regularity seam in Recognition Science would cite this step. The proof obtains differentiability from the ContDiff assumption, builds HasDerivAt expressions for the translated copies via the chain rule, equates the two sides of the original equation after differentiation, and simplifies the resulting identity.
Claim. Let $H : ℝ → ℝ$ be twice continuously differentiable and obey $H(t+u) + H(t-u) = 2 H(t) H(u)$ for all real $t,u$. Then $H'(t+u) - H'(t-u) = 2 H(t) H'(u)$ for all real $t,u$.
background
The d'Alembert equation is the functional equation $H(t+u) + H(t-u) = 2 H(t) H(u)$. The module ContDiffReduction removes an explicit regularity seam for T5 by showing that any ContDiff ℝ 2 solution satisfies the ODE $H'' = H$. The supporting lemma contDiffTwo_differentiable states that ContDiff ℝ 2 Hf implies Differentiable ℝ Hf. Upstream arithmetic definitions supply the multiplication and composition operations used in the right-hand side.
proof idea
The tactic proof intros t and u, invokes contDiffTwo_differentiable to obtain differentiability, constructs HasDerivAt for the plus-shift and minus-shift via chain rule on the linear inner maps, adds those to obtain the left-side derivative, sets the constant-times-Hf right side, proves the two sides are identical functions by the d'Alembert hypothesis, applies congrArg to pass to derivatives at u, and rewrites using the HasDerivAt properties.
why it matters
This result is the immediate predecessor of dAlembert_second_deriv_at_zero_of_contDiff, which extracts the second-derivative relation at zero. It advances the module goal of deriving the ODE H'' = H on the ContDiff surface from the Recognition Composition Law and normalization alone, thereby supporting the T5 J-uniqueness step in the forcing chain without additional regularity hypotheses.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.