defect_symmetric
plain-language theorem explainer
Symmetry of the d'Alembert defect holds for even H: Δ_H(t,u) equals Δ_H(u,t) for all real t and u. Analysts deriving stability bounds for approximate solutions to the d'Alembert equation cite this to halve the cases in error estimates. The proof is a short tactic sequence that expands the defect definition, applies add_comm and the evenness hypothesis to equate arguments, then simplifies algebraically.
Claim. Let $H:ℝ→ℝ$ be even. Then for all real $t,u$, the defect satisfies $Δ_H(t,u)=Δ_H(u,t)$, where $Δ_H(t,u):=H(t+u)+H(t-u)-2H(t)H(u)$.
background
The d'Alembert defect is defined in this module as $Δ_H(t,u):=H(t+u)+H(t-u)-2H(t)H(u)$, measuring deviation from the identity $H(t+u)+H(t-u)=2H(t)H(u)$. The function H is the shifted cost $H(x)=J(x)+1$, where J satisfies the Recognition Composition Law; under this reparametrization the RCL becomes the standard d'Alembert equation. The module develops quantitative stability for near-solutions when H is even, C³, and H(0)=1, with the defect bounded on compact squares.
proof idea
The tactic proof first simplifies the defect definition. It then obtains t+u=u+t by add_comm and shows H(t-u)=H(u-t) by rewriting t-u=-(u-t) and applying the even hypothesis. The two equalities are substituted back, after which ring closes the identity.
why it matters
This lemma supplies a basic symmetry property used throughout the d'Alembert stability development that follows the paper by Washburn and Zlatanović. It rests on the H reparametrization that converts the Recognition Composition Law into d'Alembert form and supports the subsequent uniform bounds and regularity statements in the module. No downstream uses are recorded in the current graph.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.