StabilityBounds
plain-language theorem explainer
StabilityBounds packages the defect tolerance ε, the uniform bound B on |H|, and the third-derivative bound K on the interval [-T, T] for a candidate solution H of the d'Alembert equation. Analysts applying quantitative stability results to near-solutions of functional equations cite this record when feeding explicit constants into truncation-error estimates. The definition is a direct record that bundles the three uniform bounds together with their non-negativity and positivity conditions.
Claim. Let $H : ℝ → ℝ$ and $T ∈ ℝ$. The stability bounds for $H$ on $[-T, T]$ consist of real numbers $ε ≥ 0$, $B > 0$, $K ≥ 0$ such that the d'Alembert defect satisfies $|Δ_H(t, u)| ≤ ε$ whenever $|t| ≤ T$ and $|u| ≤ T$, the function satisfies $|H(t)| ≤ B$ for all $|t| ≤ T$, and the third derivative satisfies $|H'''(t)| ≤ K$ for all $|t| ≤ T$, where $Δ_H(t, u) := H(t+u) + H(t-u) - 2 H(t) H(u)$.
background
The d'Alembert equation $H(t+u) + H(t-u) = 2 H(t) H(u)$ is obtained in Recognition Science by the shift $H(x) = J(x) + 1$, where the Recognition Composition Law for the cost $J$ becomes the standard d'Alembert identity under this map. The defect is $Δ_H(t, u) := H(t+u) + H(t-u) - 2 H(t) H(u)$. UniformDefectBound H T ε is the proposition that this defect remains at most ε throughout the square $[-T, T]^2$.
proof idea
StabilityBounds is introduced as a structure that directly records the three bounds ε, B, K together with the propositions ε_nonneg, B_pos, K_nonneg and the three uniform bound statements. No tactics are required; the definition serves as a hypothesis bundle for downstream results such as dAlembert_stability and cost_stability_transfer.
why it matters
This record supplies the concrete constants required by the stability theorem dAlembert_stability and the cost-transfer results cost_stability_calibrated and cost_stability_transfer. It bridges the abstract defect derived from the Recognition Composition Law (via H = J + 1) to the explicit error function δ(h) = ε/h² + (1+B) K h /3 that controls proximity to cosh(√a t) on the interval [-T, T]. The construction supports transfer from the functional equation to the cost functional F.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.