StabilityFromODEHypothesis
plain-language theorem explainer
This interface posits that an ODE approximation derived from a small d'Alembert defect implies an explicit stability bound on the deviation of H from cosh. Researchers formalizing quantitative stability for functional equations in Recognition Science would cite it when transferring defect controls to error estimates on the cost representation. The proof shape is a direct implication statement justified by the variation-of-parameters integral formula with remainder bounded by δ/a times (cosh - 1).
Claim. Let $H : ℝ → ℝ$ be $C^3$ and even with $H(0) = 1$ and curvature $a = H''(0) > 0$, and let the uniform defect satisfy $|Δ_H(t,u)| ≤ ε$ together with bounds $|H| ≤ B$ and $|H'''| ≤ K$ on $[-T,T]$. If the ODE approximation $|H''(t) - a H(t)| ≤ δ$ holds for $|t| ≤ T - h$, then the stability estimate $|H(t) - cosh(√a · t)| ≤ (δ/a)(cosh(√a · |t|) - 1)$ follows for the same range.
background
The module formalizes stability for near-solutions of the d'Alembert equation $H(t+u) + H(t-u) = 2 H(t) H(u)$, with defect $Δ_H(t,u) := H(t+u) + H(t-u) - 2 H(t) H(u)$. StabilityHypotheses packages the standing assumptions: $H$ is $C^3$ on $[-T,T]$, even, normalized by $H(0)=1$, and has positive curvature $a = H''(0)$. StabilityBounds supplies the concrete constants ε (defect), B (function size), and K (third-derivative size) together with the uniform-defect predicate UniformDefectBound.
proof idea
This is a one-line wrapper that states the implication ODEApproximation H T a bounds → StabilityEstimate H T a bounds. The supporting argument, recorded in the declaration's doc-comment, invokes the variation-of-parameters formula for the inhomogeneous linear ODE $H'' - a H = r$ with $|r| ≤ δ$, producing the integral representation whose absolute value is then bounded by (δ/a)(cosh(√a |t|) - 1).
why it matters
The declaration supplies the missing logical link inside dAlembert_stability (Theorem 7.1) and is invoked directly by stability_from_ode_approx. It thereby completes the quantitative passage from defect bounds on the cost-derived function H = J + 1 to explicit closeness to cosh, supporting the Recognition Science transfer from the RCL to hyperbolic representations and the phi-ladder mass formulas.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.