defect_symmetric
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.
claimLet $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 in Recognition Science
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.
scope and limits
- Does not prove the defect is identically zero.
- Does not assume any differentiability or continuity of H.
- Does not apply when H fails to be even.
- Does not supply quantitative size bounds on the defect.
formal statement (Lean)
97lemma defect_symmetric (H : ℝ → ℝ) (hEven : Function.Even H) (t u : ℝ) :
98 dAlembertDefect H t u = dAlembertDefect H u t := by
proof body
Tactic-mode proof.
99 simp only [dAlembertDefect]
100 have h1 : t + u = u + t := add_comm t u
101 have h2 : H (t - u) = H (u - t) := by
102 calc H (t - u) = H (-(u - t)) := by ring_nf
103 _ = H (u - t) := hEven _
104 rw [h1, h2]
105 ring
106
107/-! ## Defect Bounds and Regularity -/
108
109/-- Uniform bound on the defect over a symmetric interval. -/