dAlembert_product
plain-language theorem explainer
Any real-valued function H satisfying the d'Alembert addition rule H(t+u) + H(t-u) = 2 H(t) H(u) with H(0)=1 must obey the product identity H(t+u) H(t-u) = H(t)^2 + H(u)^2 - 1. Researchers proving uniqueness of the J-cost function at T5 in Recognition Science cite this algebraic step. The proof instantiates the addition hypothesis at (t+u, t-u), invokes the double-angle lemma twice, and closes the resulting equation with linear arithmetic.
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+u) H(t-u) = H(t)^2 + H(u)^2 - 1$ for all real $t,u$.
background
The module supplies helper lemmas for the T5 cost uniqueness proof. H is the reparametrization H(t) = G(t) + 1 of the underlying cost function G, chosen so that the Recognition Composition Law converts into the classical d'Alembert equation. Upstream, the definition H(x) = J(x) + 1 = ½(x + x^{-1}) makes this conversion explicit. The sibling lemma dAlembert_double supplies the auxiliary identity H(2t) = 2 (H t)^2 - 1 that the argument requires.
proof idea
The tactic proof introduces t and u, instantiates h_dAlembert at (t+u, t-u) to produce H(2t) + H(2u) = 2 H(t+u) H(t-u), applies dAlembert_double to both sides to replace the left-hand side, and finishes with a short calc block followed by linarith.
why it matters
The lemma supplies the product identity required by the immediate downstream result dAlembert_diff_square, which itself feeds the T5 J-uniqueness argument. It therefore closes one algebraic link between the Recognition Composition Law and the explicit form of J at the self-similar fixed point. The step is internal to the forcing chain that forces D = 3 and the eight-tick octave.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.