defect_even_in_t
plain-language theorem explainer
The lemma establishes that the d'Alembert defect Δ_H(t,u) is invariant under sign flip of the first argument when H is even. Researchers deriving stability bounds for approximate solutions to the d'Alembert equation in Recognition Science cite this symmetry to halve the domain in error estimates. The proof is a tactic-mode algebraic verification that applies evenness to four terms and cancels the difference by ring normalization.
Claim. If $H:ℝ→ℝ$ is even, then $Δ_H(t,u)=Δ_H(-t,u)$ for all real $t,u$, where $Δ_H(t,u):=H(t+u)+H(t-u)-2H(t)H(u)$.
background
The D'Alembert Stability Theory module develops quantitative bounds for near-solutions of the functional equation H(t+u)+H(t-u)=2H(t)H(u). The defect Δ_H(t,u) is defined exactly as the deviation H(t+u)+H(t-u)-2H(t)H(u), per the upstream dAlembertDefect declaration. The function H itself is the shifted cost H(x)=J(x)+1, which converts the Recognition Composition Law into the classical d'Alembert identity, as stated in the CostAlgebra.H definition.
proof idea
The tactic proof begins by unfolding the defect definition. Three auxiliary facts are derived by ring normalization followed by application of the evenness hypothesis: H(t+u)=H(-t-u), H(t-u)=H(-t+u), and H(t)=H(-t). These identities are substituted into the expanded expressions for both defects, after which a final ring step confirms the two sides are identical.
why it matters
The result supplies a basic symmetry needed for the stability estimates and UniformDefectBound lemmas in the same module, which in turn support the Stability Theorem (Theorem 7.1) and Cost Stability Corollary described in the module documentation. It rests on the transformation of the Recognition Composition Law into d'Alembert form via H=J+1 and on the T5 J-uniqueness step of the forcing chain. No open scaffolding is closed here; the lemma is purely algebraic.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.