dAlembert_solution_even
Any function H satisfying the d'Alembert equation H(t+u) + H(t-u) = 2 H(t) H(u) together with H(0)=1 must be even. Recognition Science applies this symmetry when reparametrizing the cost functional into additive coordinates prior to deriving the derivative condition and uniqueness. The proof is a direct one-line substitution of the first argument to zero followed by algebraic rearrangement using the normalization.
claimIf 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(-t) = H(t)$ for all $t$.
background
In the Recognition Science setting the cost functional F is transformed to log-coordinates via G(t) = F(exp t), after which the shifted map H = G + 1 obeys the d'Alembert equation. The upstream CostAlgebra result states that the shifted J-cost satisfies H(x) = ½(x + x⁻¹) and converts the Recognition Composition Law into precisely this additive form. The module proves that the d'Alembert equation is the unique low-complexity combiner compatible with symmetry, normalization at 1, and quadratic dependence.
proof idea
Extract the normalization H(0)=1 and the functional equation from the IsDAlembertSolution hypothesis. Instantiate the equation at the first argument zero to obtain H(u) + H(-u) = 2 H(u). Apply the zero-addition lemma together with two-multiplication, then finish by linear arithmetic.
why it matters in Recognition Science
The result is invoked directly by dAlembert_solution_deriv_zero to conclude that the derivative vanishes at the origin for differentiable solutions. It supplies the even symmetry required in the module's proof outline before constraining the combiner Φ and establishing uniqueness of the d'Alembert form under the Recognition Composition Law. The step aligns with the forcing chain by confirming the symmetry needed prior to the eight-tick octave and spatial dimension count.
scope and limits
- Does not prove that every solution is of cosh form.
- Does not assume or use differentiability of H.
- Does not treat solutions over the complex numbers.
- Does not establish the converse implication for even functions.
- Does not bound the growth of H.
Lean usage
have hEven := dAlembert_solution_even H h; exact even_deriv_at_zero H hEven hDiffformal statement (Lean)
111theorem dAlembert_solution_even (H : ℝ → ℝ) (h : IsDAlembertSolution H) :
112 Function.Even H := by
proof body
Term-mode proof.
113 have h0 := h.1
114 have heq := h.2
115 intro u
116 have := heq 0 u
117 simp only [zero_add, zero_sub, h0, two_mul] at this
118 linarith
119
120/-- D'Alembert solutions satisfy H'(0) = 0 if differentiable. -/