defect_even_in_u
plain-language theorem explainer
The lemma shows that the d'Alembert defect satisfies Δ_H(t,u) = Δ_H(t,-u) for any even function H. Workers on stability bounds for approximate solutions to the d'Alembert equation cite this symmetry when controlling error terms over symmetric intervals. The proof is a direct algebraic reduction: it unfolds the defect definition, applies evenness to equate H(u) with H(-u), rewrites the sign-flipped arguments via ring, and normalizes the resulting expression.
Claim. If $H:ℝ→ℝ$ is even, then for all real $t,u$ the defect satisfies $Δ_H(t,u)=Δ_H(t,-u)$, where $Δ_H(t,u):=H(t+u)+H(t-u)-2H(t)H(u)$.
background
The module develops stability estimates for near-solutions of the d'Alembert functional equation $H(t+u)+H(t-u)=2H(t)H(u)$. The defect is defined as $Δ_H(t,u):=H(t+u)+H(t-u)-2H(t)H(u)$; it vanishes exactly when the equation holds at the point $(t,u)$. Upstream, the shifted cost $H(x)=J(x)+1$ converts the Recognition Composition Law into this d'Alembert form, with $H$ even by construction from the reciprocal property of $J$. The local setting assumes $H$ even with $H(0)=1$ and prepares quantitative closeness to $cosh(√a·t)$ when the defect is small.
proof idea
The tactic proof unfolds the defect definition via simp. It extracts $H(u)=H(-u)$ from the evenness hypothesis, rewrites the arguments $t-(-u)$ and $t+(-u)$ to $t+u$ and $t-u$ by ring, substitutes the evenness equality, and finishes with ring normalization to obtain syntactic identity.
why it matters
This symmetry lemma belongs to the suite of defect properties (even in $t$, symmetric, zero iff exact solution) that support the quantitative stability theorem for approximate d'Alembert solutions. It closes a basic algebraic step needed before applying $C^3$ bounds or transferring error to the cost functional $F$. In the Recognition chain it reinforces the passage from the RCL through the eight-tick octave to $D=3$ by ensuring defect estimates remain consistent under sign flip in the time-like variable.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.