dAlembertDefect
plain-language theorem explainer
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
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.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.