dAlembert_even
plain-language theorem explainer
Any real-valued function H satisfying H(0)=1 and the d'Alembert relation H(t+u)+H(t-u)=2 H(t) H(u) for all real t,u must be even. Workers on the T5 cost-uniqueness argument in Recognition Science cite the result to enforce reciprocal symmetry before classifying solutions. The argument is a direct specialization of the functional equation at t=0 followed by algebraic cancellation using the normalization condition.
Claim. Let $H : ℝ → ℝ$. If $H(0)=1$ and $H(t+u)+H(t-u)=2 H(t) H(u)$ for all $t,u ∈ ℝ$, then $H(-x)=H(x)$ for all $x ∈ ℝ$.
background
In the Recognition Science cost module the auxiliary map H is defined by H_F(t) = G_F(t) + 1, where G_F is the original cost function. Under this shift the Recognition Composition Law becomes the additive d'Alembert equation H(t+u) + H(t-u) = 2 H(t) H(u). The present module supplies elementary lemmas that support the T5 J-uniqueness proof by establishing basic properties of such H before regularity or classification arguments are applied.
proof idea
Specialize the d'Alembert hypothesis at t=0 to obtain H(u) + H(-u) = 2 H(0) H(u). Substitute the given normalization H(0)=1, invoke zero_add to replace the zero term, and apply the identities sub_eq_add_neg and two_mul. The resulting equality H(u) + H(-u) = 2 H(u) rearranges directly to evenness. The proof is a one-line term-mode simplification.
why it matters
The lemma is invoked by dAlembert_classification and dAlembert_contDiff_top to guarantee that candidate solutions are even before they are identified with cosh or cos. It supplies an early step in the T5 forcing chain that converts the Recognition Composition Law into the standard d'Alembert form via the shifted cost H(x) = J(x) + 1. Downstream results such as dAlembert_cosh_solution and composition_law_forces_reciprocity rely on this evenness to calibrate the second derivative at zero and to close the uniqueness argument.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.