Explanation of the lemma dAlembert_double

(1) In plain English, the declaration asserts that any real-valued function H obeying H(0) = 1 and the two-variable functional equation H(t + u) + H(t - u) = 2 · H(t) · H(u) for all real t and u must also satisfy the double-step identity H(2t) = 2 · (H(t))² - 1. This is obtained simply by substituting u = t into the given equation and rearranging with elementary arithmetic.

(2) The lemma supports the functional-equation analysis inside the Cost module that underpins the uniqueness argument for the reciprocal-symmetric cost function J. By supplying a concrete algebraic consequence of the d'Alembert relation, it contributes to the chain that isolates the unique cost expression used for the recognition ledger.

(3) The formal statement is read as follows: the lemma is parameterized by a function H : ℝ → ℝ together with two hypotheses (h_one : H 0 = 1 and h_dAlembert : ∀ t u, H (t + u) + H (t - u) = 2 * H t * H u) and an arbitrary real argument t. Its conclusion is the equality H (2 * t) = 2 * (H t)^2 - 1. The proof proceeds by instantiating h_dAlembert at (t, t), invoking h_one to replace the H(0) term, and simplifying the resulting linear equation.

(4) Visible dependencies inside the supplied source are the hypothesis h_dAlembert (used directly) and the tactics linarith and simpa for the arithmetic steps. The lemma is invoked by the subsequent declaration dAlembert_product, which applies it twice to obtain a product identity. Related declarations in the same module include dAlembert_even and Jcost_cosh_add_identity.

(5) The declaration does not prove that any particular function (such as Jcost) satisfies the d'Alembert equation, nor does it establish existence, uniqueness, or smoothness of solutions. It likewise contains no statements about phi, the forcing chain, or derived physical constants; those connections lie outside this single lemma.