dAlembert_stability
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.
claimLet $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 in Recognition Science
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.
scope and limits
- Does not establish the ODE approximation step without the separate lemma ode_approximation_from_defect.
- Does not extend the bounds beyond the compact interval [-T,T].
- Does not relax the C³ smoothness or evenness requirements on H.
- Does not remove dependence on the third-derivative bound K inside δ_error.
formal statement (Lean)
254theorem dAlembert_stability
255 (H : ℝ → ℝ) (T : ℝ) (hyp : StabilityHypotheses H T) (bounds : StabilityBounds H T)
256 (h_ode : ODEApproximationHypothesis H T hyp bounds)
257 (h_stab : StabilityFromODEHypothesis H T hyp bounds) :
258 StabilityEstimate H T hyp.curvature bounds := by
proof body
Term-mode proof.
259 have h_ode' := ode_approximation_from_defect H T hyp bounds h_ode
260 exact stability_from_ode_approx H T hyp bounds h_ode' h_stab
261
262/-! ## Corollary 7.1: Stability for the Cost Functional -/
263
264/-- **Corollary 7.1 (Cost Functional Stability)**
265
266Let F(x) := H(log x) - 1 on ℝ₊, where H satisfies the stability hypotheses.
267
268If a is close to 1 and δ(h) is small, then F is uniformly close to the
269canonical cost J(x) = cosh(log x) - 1 on compact subintervals of (0, ∞).
270
271When a = 1, the estimate simplifies to:
272 |F(x) - J(x)| ≤ δ(h) · J(|x|) -/