dAlembert_even_solution
plain-language theorem explainer
Any real function H satisfying the d'Alembert relation H(t+u) + H(t-u) = 2 H(t) H(u) together with H(0)=1 is even. Workers on the Recognition Composition Law cite the result to obtain symmetry before passing to the ODE that forces the cosh solution. The proof is a one-line wrapper that invokes the dAlembert_even lemma.
Claim. Let $H : ℝ → ℝ$ satisfy $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 Full Unconditional module the cost function is reparametrized by the shifted map H(x) = J(x) + 1, where J(x) = (x + x^{-1})/2 - 1. Under this change the Recognition Composition Law becomes the d'Alembert equation H(xy) + H(x/y) = 2 H(x) H(y). The module proves that any F obeying normalization F(1)=0, reciprocal symmetry, C² smoothness, the calibration G''(0)=1, and multiplicative consistency for some P must satisfy F = J and P(u,v) = 2uv + 2u + 2v.
proof idea
The proof is a one-line wrapper that applies the lemma dAlembert_even from Cost.FunctionalEquation, supplying the normalization H(0)=1 and the d'Alembert relation as arguments.
why it matters
The declaration removes an evenness hypothesis that earlier partial versions of RCL inevitability carried. It supplies the symmetry step required before the ODE uniqueness theorem ode_cosh_uniqueness_contdiff can be invoked to force H = cosh and therefore F = J. The result sits inside the forcing chain that derives J-uniqueness (T5) and the Recognition Composition Law from the single functional equation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.