ode_approximation_from_defect
plain-language theorem explainer
The declaration shows that the ODE approximation hypothesis for a function H satisfying stability hypotheses and bounds directly implies the ODE approximation property, namely that the second derivative deviates from a times H by at most a small δ depending on the defect bound. Researchers deriving differential approximations from functional defects in Recognition Science cite this when moving from the d'Alembert equation to local ODE control. The proof is a one-line wrapper that applies the hypothesis definition.
Claim. Let $H : ℝ → ℝ$ and $T > 0$. Assume $H$ is $C^3$, even, normalized by $H(0) = 1$, with positive curvature $a = H''(0)$, and satisfies the uniform defect bound $ε$, bound $B$ on $|H|$, and bound $K$ on $|H'''|$. If the ODE approximation hypothesis holds, then $|H''(t) - a H(t)| ≤ δ(ε, B, K, h)$ for all $0 < h ≤ T$ and $|t| ≤ T - h$.
background
The D'Alembert Stability Theory module formalizes stability estimates for near-solutions of the d'Alembert functional 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 bundles the assumptions that $H$ is $C^3$ and even with $H(0) = 1$ and positive second derivative $a$ at zero. StabilityBounds supplies the uniform defect bound $ε$, the bound $B$ on $|H|$, and $K$ on $|H'''|$. The upstream CostAlgebra result defines $H(x) = J(x) + 1$, converting the Recognition Composition Law into the d'Alembert equation.
proof idea
The proof is a one-line wrapper that applies the definition of ODEApproximationHypothesis, which is identical to the target ODEApproximation property.
why it matters
This lemma supplies the ODE intermediate step in the proof of the main d'Alembert stability theorem (Theorem 7.1) and is invoked directly by the downstream dAlembert_stability result. It fills the passage from functional defect to differential approximation in the Recognition Science chain, linking the RCL to quantitative bounds on near-solutions of the cost functional. It touches the open question of explicit error control for the phi-ladder mass formula.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.