dAlembert_even'
plain-language theorem explainer
Every solution of the d'Alembert equation H(t+u) + H(t-u) = 2 H(t) H(u) with H(0)=1 is an even function. Researchers working on functional equations or the Recognition Science cost model cite this symmetry as the initial step in the Aczél classification. The proof substitutes zero into the functional equation twice and applies linear arithmetic after simplification with the normalization H(0)=1.
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 real $t$.
background
In the Recognition Science framework the cost function is reparametrized via the shifted map H(x) = J(x) + 1, where J satisfies the Recognition Composition Law. This converts the RCL into the additive d'Alembert equation H(t+u) + H(t-u) = 2 H(t) H(u). The present theorem records the evenness property for any such H on the reals. The module develops the full Aczél smoothness argument showing that continuous solutions are C^∞ and fall into the constant, cosh, or cosine families. Upstream definitions supply H both as J+1 in the algebra module and as the convenience wrapper G_F + 1 in the functional-equation module.
proof idea
The proof is a short term-mode argument. Introduce t. Apply the d'Alembert hypothesis at (0,t) to obtain H(t) + H(-t) = 2 H(0) H(t). Simplify with H(0)=1 to reach H(t) + H(-t) = 2 H(t). The symmetric substitution at (0,-t) produces the identical relation. Linear arithmetic then forces H(-t) = H(t).
why it matters
This is the first lemma (labeled H1) in the Aczél smoothness chain inside the Cost domain. It supplies the symmetry needed for the representation formula and regularity bootstrap that ultimately discharge the former H_AczelClassification hypothesis. In the broader framework the evenness of H is required for the phi-ladder mass formulas and the eight-tick octave structure. No open questions attach to this specific statement.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.