UniformDefectBound
plain-language theorem explainer
UniformDefectBound asserts that the d'Alembert defect of a map H stays at most ε throughout the square interval of radius T. Analysts working on stability estimates for functional equations cite it to state the small-defect hypothesis in quantitative bounds. The definition is a direct universal quantification of the absolute defect over the compact domain.
Claim. Let $H : ℝ → ℝ$. The uniform defect bound on $[-T,T]^2$ with tolerance $ε$ holds when $|H(t+u) + H(t-u) - 2 H(t) H(u)| ≤ ε$ for all real $t,u$ with $|t| ≤ T$ and $|u| ≤ T$.
background
The module develops stability estimates for near-solutions of the d'Alembert equation $H(t+u) + H(t-u) = 2 H(t) H(u)$. The defect at a point is the pointwise failure $Δ_H(t,u) := H(t+u) + H(t-u) - 2 H(t) H(u)$, which vanishes exactly when the identity holds. Upstream, $H$ arises as the shifted cost $H(x) = J(x) + 1$ from the cost algebra, where $J$ satisfies the recognition composition law that forces the d'Alembert identity exactly.
proof idea
This is a definition that directly encodes the uniform bound as a universal statement over the interval $[-T,T]$ for both variables, using the already-defined defect expression.
why it matters
This predicate appears in the StabilityBounds record as the defect_bound field and is invoked in the zero-defect theorems to recover exact cosh solutions. It implements the small-defect hypothesis of the stability theorem (Theorem 7.1) in the cited paper on uniqueness of the canonical reciprocal cost, linking to the Recognition Science framework where J-uniqueness produces the cosh form.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.