dAlembert_solution_even
plain-language theorem explainer
Any function H satisfying the d'Alembert equation H(t+u) + H(t-u) = 2 H(t) H(u) together with H(0)=1 must be even. Recognition Science applies this symmetry when reparametrizing the cost functional into additive coordinates prior to deriving the derivative condition and uniqueness. The proof is a direct one-line substitution of the first argument to zero followed by algebraic rearrangement using the normalization.
Claim. If a function $H : ℝ → ℝ$ satisfies $H(0) = 1$ and $H(t + u) + H(t - u) = 2 H(t) H(u)$ for all real $t, u$, then $H(-t) = H(t)$ for all $t$.
background
In the Recognition Science setting the cost functional F is transformed to log-coordinates via G(t) = F(exp t), after which the shifted map H = G + 1 obeys the d'Alembert equation. The upstream CostAlgebra result states that the shifted J-cost satisfies H(x) = ½(x + x⁻¹) and converts the Recognition Composition Law into precisely this additive form. The module proves that the d'Alembert equation is the unique low-complexity combiner compatible with symmetry, normalization at 1, and quadratic dependence.
proof idea
Extract the normalization H(0)=1 and the functional equation from the IsDAlembertSolution hypothesis. Instantiate the equation at the first argument zero to obtain H(u) + H(-u) = 2 H(u). Apply the zero-addition lemma together with two-multiplication, then finish by linear arithmetic.
why it matters
The result is invoked directly by dAlembert_solution_deriv_zero to conclude that the derivative vanishes at the origin for differentiable solutions. It supplies the even symmetry required in the module's proof outline before constraining the combiner Φ and establishing uniqueness of the d'Alembert form under the Recognition Composition Law. The step aligns with the forcing chain by confirming the symmetry needed prior to the eight-tick octave and spatial dimension count.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.