dAlembert_even
Any real-valued function H satisfying H(0) = 1 and the d'Alembert equation H(t+u) + H(t-u) = 2 H(t) H(u) for all real t and u must be even. Researchers deriving the explicit form of the cost function in Recognition Science cite this lemma to obtain the required symmetry before classification. The argument is a direct substitution of t = 0 into the functional equation followed by algebraic simplification with the normalization condition.
claimLet $H : ℝ → ℝ$ satisfy $H(0) = 1$ and $H(t + u) + H(t - u) = 2 H(t) H(u)$ for all real $t, u$. Then $H$ is even: $H(-x) = H(x)$ for every real $x$.
background
The Cost.FunctionalEquation module supplies lemmas for the T5 cost uniqueness proof. Here H is the shifted cost function defined by H(t) := G(t) + 1, where G obeys the Recognition Composition Law; the given equation is the additive d'Alembert form of that law after the shift. The upstream definition in CostAlgebra states that the canonical H satisfies H(x) = J(x) + 1 = ½(x + x^{-1}), which is even by inspection.
proof idea
This is a one-line term-mode proof. Instantiate the d'Alembert hypothesis at t = 0 to obtain H(u) + H(-u) = 2 H(0) H(u). The assumption H(0) = 1 together with zero_add and sub_eq_add_neg reduces the right-hand side to 2 H(u), after which cancellation yields evenness.
why it matters in Recognition Science
The evenness result is invoked by dAlembert_classification in AczelProof and by dAlembert_cosh_solution together with dAlembert_cosh_solution_aczel. It supplies the symmetry needed to reduce the general d'Alembert equation to the standard form whose continuous solutions are cosh(α·), cos(α·), or the constant 1. In the Recognition framework this step confirms that the cost function inherits the even symmetry forced by the J-cost at T5, advancing the derivation of J(x) = cosh(log x) - 1.
scope and limits
- Does not assume continuity or differentiability of H.
- Establishes only evenness and does not classify solutions.
- Applies exclusively to the additive d'Alembert equation over the reals.
- Does not treat the original multiplicative form of the Recognition Composition Law.
formal statement (Lean)
97lemma dAlembert_even
98 (H : ℝ → ℝ)
99 (h_one : H 0 = 1)
100 (h_dAlembert : ∀ t u, H (t+u) + H (t-u) = 2 * H t * H u) :
101 Function.Even H := by
proof body
Term-mode proof.
102 intro u
103 have h := h_dAlembert 0 u
104 simpa [h_one, zero_add, sub_eq_add_neg, two_mul] using h
105