defect_zero_iff_dAlembert
plain-language theorem explainer
The lemma equates vanishing of the d'Alembert defect to satisfaction of the functional equation H(t+u) + H(t-u) = 2 H(t) H(u). Researchers working on stability of approximate solutions to d'Alembert's equation would cite this equivalence when bounding deviations from cosh-like behavior. The proof is a direct simplification using the definition of the defect and the fact that subtraction yields zero.
Claim. For any function $H : ℝ → ℝ$, the d'Alembert defect at $(t,u)$ vanishes if and only if $H(t + u) + H(t - u) = 2 · H(t) · H(u)$, where the defect is defined by $Δ_H(t,u) := H(t+u) + H(t-u) - 2 · H(t) · H(u)$.
background
The d'Alembert defect is defined as Δ_H(t,u) := H(t+u) + H(t-u) - 2·H(t)·H(u). This measures deviation from the d'Alembert functional equation H(t+u) + H(t-u) = 2·H(t)·H(u). In the Recognition Science setting, H arises as the shifted cost H(x) = J(x) + 1, under which the Recognition Composition Law becomes the d'Alembert equation. The module develops stability estimates for near-solutions of this equation, following the development in J. Washburn & M. Zlatanović, Uniqueness of the Canonical Reciprocal Cost, with the defect serving as the central quantitative measure of approximation quality.
proof idea
The proof is a one-line term-mode simplification that unfolds the definition of dAlembertDefect and applies the lemma sub_eq_zero to obtain the equivalence.
why it matters
This equivalence underpins the stability estimates in the D'Alembert Stability module, which transfers to cost functional stability via the reparametrization H = J + 1. It connects directly to the Recognition Composition Law and supports the quantitative bounds when the defect is small, as outlined in the module's stability theorem and cost stability corollary. The result fills Definition 7.1 in the module and enables the transfer from algebraic identities to analytic stability statements.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.