dAlembertDefect
The d'Alembert defect quantifies deviation of a map H from the identity H(t+u) + H(t-u) = 2 H(t) H(u). Researchers deriving stability bounds for the Recognition Science cost functional or approximate solutions to functional equations cite this quantity when controlling residuals. It is introduced by the direct algebraic expression H(t+u) + H(t-u) - 2 H(t) H(u) that feeds every subsequent symmetry and bound statement in the module.
claim$Δ_H(t,u) := H(t+u) + H(t-u) - 2 H(t) H(u)$ for a function $H:ℝ→ℝ$.
background
The module develops quantitative stability for near-solutions of the d'Alembert equation that arises once the Recognition Composition Law is rewritten under the shifted cost. Upstream CostAlgebra.H supplies the reparametrization H(x) = J(x) + 1, which converts the multiplicative RCL into the additive form H(xy) + H(x/y) = 2 H(x) H(y). The same H appears in the module's local setting as the target of stability estimates when H is even, C³, and normalized by H(0) = 1.
proof idea
One-line definition that subtracts the right-hand side of the d'Alembert identity from its left-hand side.
why it matters in Recognition Science
This definition supplies the central residual for the stability theorem and cost-stability corollary of the module, which in turn rest on the J-uniqueness step (T5) of the forcing chain. Downstream lemmas defect_zero_iff_dAlembert, defect_symmetric and UniformDefectBound all invoke it directly; the quantity therefore bridges the exact cosh solution of the cost functional to its approximate versions inside the eight-tick octave framework.
scope and limits
- Does not assume continuity, differentiability or evenness of H.
- Does not derive any size bound on the defect.
- Does not connect the defect to the phi-ladder or mass formula.
- Does not treat the multiplicative form of the equation.
formal statement (Lean)
57def dAlembertDefect (H : ℝ → ℝ) (t u : ℝ) : ℝ :=
proof body
Definition body.
58 H (t + u) + H (t - u) - 2 * H t * H u
59
60/-- The defect is zero iff H satisfies the d'Alembert equation at (t, u). -/