ODEApproximationHypothesis
The declaration posits the ODE approximation |H''(t) - a H(t)| ≤ δ(ε,B,K,h) as an explicit hypothesis on a C³ even function normalized at zero. Stability analysts working with near-solutions to the d'Alembert equation cite it to convert uniform defect bounds into pointwise differential control before invoking the full stability estimate. The definition is a one-line wrapper that directly instantiates the ODEApproximation predicate at the supplied curvature.
claimLet $H:ℝ→ℝ$ and $T>0$. Assume $H$ is $C^3$, even, satisfies $H(0)=1$ and $H''(0)=a>0$, and obeys uniform bounds $|Δ_H(t,u)|≤ε$, $|H(t)|≤B$, $|H'''(t)|≤K$ on $[-T,T]$. Then $|H''(t)-a H(t)|≤δ(ε,B,K,h)$ holds for all $0<h≤T$ and $|t|≤T-h$.
background
The d'Alembert equation is $H(t+u)+H(t-u)=2H(t)H(u)$, with defect $Δ_H(t,u):=H(t+u)+H(t-u)-2H(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 numerical controls: defect bounded by $ε≥0$, range bounded by $B>0$, and third derivative bounded by $K$.
proof idea
The definition is a one-line wrapper that returns the ODEApproximation predicate instantiated at hyp.curvature. No tactics or reductions occur inside the body; the predicate itself encodes the Taylor expansion of $H(t+h)+H(t-h)$ combined with the defect identity and the supplied bounds on $H'''$.
why it matters in Recognition Science
It supplies the missing ODE-control hypothesis inside dAlembert_stability (Theorem 7.1) and is discharged by ode_approximation_from_defect. The step completes the passage from defect estimates to the differential inequality that yields the cosh-type stability bound, supporting the transfer from the Recognition Composition Law (via CostAlgebra.H) to local hyperbolic behavior on finite intervals.
scope and limits
- Does not derive the ODE bound from the defect identity.
- Does not supply an explicit formula for the error function δ_error.
- Does not extend the approximation beyond the interval [-T,T].
- Does not relax the C³ regularity or evenness assumptions.
falsifier
A C³ even function H with H(0)=1, H''(0)=a>0, defect ≤ε, |H|≤B and |H'''|≤K on [-T,T] yet |H''(t)-a H(t)| > δ(ε,B,K,h) for some admissible h and t would falsify the hypothesis.
Lean usage
theorem dAlembert_stability (H : ℝ → ℝ) (T : ℝ) (hyp : StabilityHypotheses H T) (bounds : StabilityBounds H T) (h_ode : ODEApproximationHypothesis H T hyp bounds) (h_stab : StabilityFromODEHypothesis H T hyp bounds) : StabilityEstimate H T hyp.curvature bounds := byformal statement (Lean)
221def ODEApproximationHypothesis
222 (H : ℝ → ℝ) (T : ℝ) (hyp : StabilityHypotheses H T) (bounds : StabilityBounds H T) : Prop :=
proof body
Definition body.
223 ODEApproximation H T hyp.curvature bounds
224