dAlembert_stability
plain-language theorem explainer
The d'Alembert stability theorem supplies explicit uniform bounds showing that any C³ even function H with H(0)=1 and small d'Alembert defect stays close to cosh(√a t) on compact intervals, where a=H''(0). Researchers in functional equations or Recognition Science cost functionals cite it to convert defect size into concrete error estimates for near-solutions. The proof is a one-line composition that first derives the ODE approximation from the defect bound and then applies the variation-of-parameters stability estimate.
Claim. Let $H:ℝ→ℝ$ be $C^3$ and even with $H(0)=1$ and $H''(0)=a>0$. Let $ε$, $B$, $K$ be the uniform defect, function, and third-derivative bounds on $[-T,T]$. If the ODE approximation $|H''(t)-aH(t)|≤δ(h)$ holds for small $h$, then $|H(t)-cosh(√a t)|≤(δ_error(ε,B,K,h)/a)(cosh(√a |t|)-1)$ for $0<h≤T$ and $|t|≤T-h$.
background
The module formalizes stability for near-solutions of the d'Alembert equation $H(t+u)+H(t-u)=2H(t)H(u)$, with defect $Δ_H(t,u):=H(t+u)+H(t-u)-2H(t)H(u)$. StabilityHypotheses bundles $C^3$ smoothness on $[-T,T]$, evenness, normalization $H(0)=1$, and positive curvature $a=H''(0)>0$. StabilityBounds packages the defect bound $ε$, the sup-norm $B$ on $H$, and the third-derivative bound $K$ on $[-T,T]$.
proof idea
The proof is a one-line wrapper that applies ode_approximation_from_defect to obtain the ODE approximation from the defect bound, then invokes stability_from_ode_approx to convert that approximation into the explicit error estimate via variation of parameters.
why it matters
This is Theorem 7.1, the central stability result of the module, which directly supports Corollary 7.1 on cost-functional stability. It closes the quantitative step from the Recognition Composition Law (which becomes d'Alembert after the shift $H=J+1$) to uniform closeness with the canonical solution, supporting T5 J-uniqueness in the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.