dAlembert_double
plain-language theorem explainer
The lemma shows that any real function H obeying H(0) equals one and the additive d'Alembert relation H(t plus u) plus H(t minus u) equals two times H(t) times H(u) must satisfy the double argument identity H of two t equals two H(t) squared minus one. Workers on the T5 J-uniqueness step in the Recognition Science forcing chain cite this when manipulating the shifted cost function. The argument proceeds by specializing the functional equation at equal arguments and applying elementary algebra.
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(2t) = 2 (H t)^2 - 1$.
background
This module supplies functional equation lemmas supporting the T5 cost uniqueness proof in Recognition Science. The function H is the shifted cost, defined by H(t) = G(t) + 1 where G is the underlying cost function from the Recognition Composition Law. Upstream results establish that under this shift the RCL takes the d'Alembert form H(xy) + H(x/y) = 2 H(x) H(y), with the additive version here obtained via logarithmic reparametrization.
proof idea
The proof specializes the d'Alembert hypothesis at u = t, yielding H(2t) + H(0) = 2 (H t)^2. It then invokes the normalization H(0) = 1, subtracts one, and applies simpa and linarith to rearrange into the target identity.
why it matters
This result feeds the sibling lemma dAlembert_product, which continues the derivation of product identities for H. It supports the T5 J-uniqueness step by providing algebraic closure properties of the shifted cost function H under the Recognition framework's forcing chain. The eight-tick octave and phi fixed point rely on such functional equation manipulations.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.