dAlembert_double_angle
plain-language theorem explainer
The double-angle formula for functions satisfying d'Alembert's equation with normalization at zero follows by direct substitution. Analysts studying functional equations in the context of Recognition Science cost models cite this step when bootstrapping regularity from the shifted cost H. The proof proceeds by a short sequence of rewrites and algebraic simplification using the given equation at equal arguments.
Claim. If a function $H:ℝ→ℝ$ satisfies $H(0)=1$ and $H(t+u)+H(t-u)=2H(t)H(u)$ for all real $t,u$, then $H(2t)=2[H(t)]^2-1$ for all real $t$.
background
In the Recognition Science cost setting the shifted function $H(x)=J(x)+1$ converts the Recognition Composition Law into d'Alembert's equation $H(xy)+H(x/y)=2H(x)H(y)$. The present module establishes that every continuous solution of the additive form $H(t+u)+H(t-u)=2H(t)H(u)$ with $H(0)=1$ is $C^∞$ and belongs to one of three families: the constant 1, cosh(λt), or cos(λt). Upstream, CostAlgebra.H records the explicit relation $H(x)=½(x+x^{-1})$ that makes the reparametrization exact.
proof idea
The tactic proof introduces the target variable t, instantiates the functional equation at equal arguments u=t, rewrites the sum and difference via ring, substitutes the normalization H(0)=1, and closes with nlinarith on the square of H(t).
why it matters
This identity supplies the first algebraic relation needed for the representation formula and regularity bootstrap that together prove the full Aczél classification inside the module. Once established, the classification removes the former H_AczelClassification hypothesis, completing the zero-sorry foundation for the cost function in the Recognition Science chain (T5 J-uniqueness through the eight-tick octave).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.