stability_from_ode_approx
plain-language theorem explainer
Given a C³ even function H with H(0)=1 and positive curvature a, together with uniform bounds on its defect ε, magnitude B, and third derivative K, the assumption that the second-derivative deviation from a·H is controlled by δ(h) and the pre-established implication from that control to the explicit error bound together yield the stability estimate |H(t) − cosh(√a t)| ≤ (δ(h)/a)(cosh(√a |t|) − 1) for |t| ≤ T−h. Analysts studying stability of functional equations cite this step when closing the argument from defect bounds to cosh proximity. The
Claim. If $H:ℝ→ℝ$ is $C^3$, even, satisfies $H(0)=1$ and $H''(0)=a>0$, and obeys the uniform defect bound $ε$, magnitude bound $B$, and third-derivative bound $K$ on $[-T,T]$, and if $|H''(t)-a H(t)|≤δ(h)$ for $|t|≤T-h$, then under the hypothesis that the ODE approximation implies the stability estimate one has $|H(t)-cosh(√a t)|≤(δ(h)/a)(cosh(√a |t|)-1)$ for $|t|≤T-h$.
background
The d'Alembert functional equation is $H(t+u)+H(t-u)=2H(t)H(u)$. The defect is $Δ_H(t,u)=H(t+u)+H(t-u)-2H(t)H(u)$. StabilityHypotheses require $H$ to be $C^3$ on $[-T,T]$, even, $H(0)=1$, and curvature $a=H''(0)>0$. StabilityBounds supply $ε≥0$ with $|Δ|≤ε$, $B>0$ with $|H|≤B$, and $K$ with $|H'''|≤K$ on the interval. ODEApproximation asserts that the defect bound forces the second-derivative deviation $|H''(t)-a H(t)|≤δ(h)$ for $|t|≤T-h$. StabilityFromODEHypothesis is the implication from that ODE control to the explicit error bound in StabilityEstimate. Upstream, the shifted cost $H=J+1$ satisfies the exact d'Alembert identity under the Recognition Composition Law.
proof idea
The proof is a one-line wrapper that applies the StabilityFromODEHypothesis implication directly to the supplied ODEApproximation fact.
why it matters
This declaration closes the local argument inside Theorem 7.1 by invoking the pre-proved implication from ODE approximation to the explicit stability bound. It is used by dAlembert_stability to obtain the full stability estimate. In the Recognition Science framework it supplies the quantitative control needed to pass from the algebraic cost functional to its differential approximation, consistent with the J-uniqueness and phi-ladder constructions elsewhere in the monolith.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.