ODEApproximation
plain-language theorem explainer
ODEApproximation encodes the condition that |H''(t) - a H(t)| stays below an error term controlled by defect bound ε, function bound B, third-derivative bound K and step h, for all |t| ≤ T - h. Researchers deriving stability estimates for near-solutions of the d'Alembert equation cite it as the explicit ODE bridge in the Recognition Science cost analysis. The definition is obtained by subtracting the scaled defect identity from the Taylor expansion of H(t + h) + H(t - h).
Claim. Let $H : ℝ → ℝ$, $T,a ∈ ℝ$ and let bounds be the StabilityBounds structure supplying uniform defect bound ε, sup-norm bound B on |H| and bound K on |H'''|. The proposition holds precisely when ∀ h > 0 with h ≤ T and ∀ t with |t| ≤ T - h we have |H''(t) - a H(t)| ≤ δ_error(ε, B, K, h).
background
The D'Alembert Stability module works with the functional equation H(t + u) + H(t - u) = 2 H(t) H(u) whose defect is Δ_H(t,u) := H(t+u) + H(t-u) - 2 H(t) H(u). StabilityBounds is the structure that packages three uniform controls on [-T,T]: the defect size ε, the pointwise bound B on |H|, and the bound K on |H'''|. The shifted cost H(x) = J(x) + 1 converts the Recognition Composition Law into this d'Alembert identity, as recorded in CostAlgebra.H.
proof idea
This is a direct definition that encodes the target inequality. The inline comment obtains the bound by subtracting the defect identity from the Taylor expansion H(t+h) + H(t-h) = 2H(t) + h² H''(t) + O(h³), isolating the curvature term a from the small-h expansion of H(h), and absorbing the remainder into δ_error.
why it matters
ODEApproximation is equation (7.3) of the paper and supplies the hypothesis for the stability theorem. It is invoked by ode_approximation_from_defect to lift the hypothesis and by stability_from_ode_approx to reach the final StabilityEstimate. In the Recognition framework it closes the passage from the functional equation satisfied by the cost H to the differential equation whose solutions generate the hyperbolic functions appearing in the phi-ladder mass formulas.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.