ode_approximation_from_defect
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.
claimLet $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 in Recognition Science
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.
scope and limits
- Does not derive the ODE approximation without the hypothesis assumption.
- Does not supply explicit numerical values for the error δ.
- Does not extend the bound beyond the interval [-T, T].
- Does not address higher-order derivatives or global-in-time stability.
Lean usage
have h_ode' := ode_approximation_from_defect H T hyp bounds h_odeformal statement (Lean)
225theorem ode_approximation_from_defect
226 (H : ℝ → ℝ) (T : ℝ) (hyp : StabilityHypotheses H T) (bounds : StabilityBounds H T)
227 (h_ode : ODEApproximationHypothesis H T hyp bounds) :
228 ODEApproximation H T hyp.curvature bounds := by
proof body
Term-mode proof.
229 exact h_ode
230
231/-- **Key Lemma**: ODE approximation + Gronwall implies stability estimate.
232
233If |H''(t) - a·H(t)| ≤ δ and H(0) = cosh(0) = 1, H'(0) = sinh(0) = 0,
234then the variation-of-parameters formula gives:
235
236 H(t) - cosh(√a·t) = ∫₀ᵗ (1/√a)·sinh(√a·(t-s))·r(s) ds
237
238where r(s) = H''(s) - a·H(s) satisfies |r(s)| ≤ δ.
239
240Bounding the integral gives:
241 |H(t) - cosh(√a·t)| ≤ (δ/a)·(cosh(√a·|t|) - 1) -/