dalembert_deriv_ode
plain-language theorem explainer
The lemma shows that any C² function obeying the d'Alembert equation f(x+y) + f(x-y) = 2 f(x) f(y) satisfies the ODE f''(x) = f''(0) f(x). Analysts reducing functional equations to linear ODEs or working in Recognition Science's derivation of hyperbolic solutions cite this step. The proof differentiates both sides twice with respect to y at y=0, computes the resulting HasDerivAt expressions separately, and equates them.
Claim. If $f : ℝ → ℝ$ is twice continuously differentiable and satisfies $f(x + y) + f(x - y) = 2 f(x) f(y)$ for all real $x, y$, then $f''(x) = f''(0) · f(x)$ for all $x$.
background
The d'Alembert equation appears in Recognition Science as the addition formula satisfied by the J-cost function after composition of automorphisms. ContDiff ℝ 2 f encodes that f possesses a continuous second derivative everywhere. The lemma resides in the Relativity.Calculus.FunctionalEquationDeriv module and supplies the differential reduction used throughout the DAlembert submodules.
proof idea
Fix x and introduce g(y) := f(x+y) + f(x-y) together with h(y) := 2 f(x) f(y). The assumption forces g = h pointwise. Separate HasDerivAt calculations establish that the first derivative of g at 0 vanishes while its second derivative at 0 equals 2 f''(x); the corresponding second derivative of h at 0 equals 2 f(x) f''(0). Equating the two second derivatives at 0 and rearranging produces the ODE.
why it matters
This reduction is invoked directly by dAlembert_classification and dAlembert_with_unit_calibration to conclude that calibrated solutions equal cosh, and by entangling_forces_hyperbolic_ode to obtain the G'' = G + 1 equation. In the framework it supports T5 J-uniqueness, where J(x) = cosh(log x) - 1, and the passage from the Recognition Composition Law to the eight-tick octave and D = 3. No open scaffolding remains at this node.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.