dalembert_deriv_ode
plain-language theorem explainer
dalembert_deriv_ode shows that any twice continuously differentiable real function obeying the d'Alembert relation f(x+y)+f(x-y)=2f(x)f(y) satisfies the linear ODE f''(x)=f''(0) f(x). Analysts deriving hyperbolic solutions from functional equations or Recognition Science cost structures cite this reduction. The tactic proof differentiates both sides twice in the auxiliary shift variable, equates the second derivatives at zero via pointwise agreement and chain-rule compositions, then divides by two.
Claim. If $f:ℝ→ℝ$ is twice continuously differentiable and satisfies $f(x+y)+f(x-y)=2f(x)f(y)$ for all real $x,y$, then $f''(x)=f''(0)·f(x)$ for all $x$.
background
The Fourth Gate module treats the d'Alembert structure as a derived cross-check after the curvature gate. The shifted cost $H(x)=J(x)+1$ converts the Recognition Composition Law into the classical d'Alembert equation $H(xy)+H(x/y)=2H(x)H(y)$. Upstream results from CostAlgebra supply the definition of $H$ together with the multiplicative properties of $J$-automorphisms that underwrite the functional equation. The module recalls that continuous solutions are precisely the hyperbolic cosines, furnishing a compact certificate path parallel to the main forcing chain.
proof idea
The proof first extracts differentiability of $f$ and $f'$ from the ContDiff 2 hypothesis. It introduces explicit HasDerivAt statements for the affine shift maps $u↦t+u$ and $u↦t-u$. For fixed $t$ the two sides of the functional equation are equated as functions of $u$; their second derivatives at $u=0$ are computed separately. The left side yields $2f''(t)$ and the right side yields $2f(t)f''(0)$. Algebraic rearrangement then produces the ODE.
why it matters
The lemma is invoked by dAlembert_classification and dAlembert_with_unit_calibration to conclude that unit-calibrated solutions equal cosh; it also appears in entangling_forces_hyperbolic_ode. In the Recognition framework it bridges the RCL form of the cost algebra (via $H=J+1$) to the ODE $G''=G+1$ that follows T5 J-uniqueness, confirming consistency with the eight-tick octave and $D=3$. It supplies the classical functional-equation route to the same hyperbolic functions used in the mass formula and alpha-band derivations.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.