IsDAlembertSolution
The definition encodes the standard d'Alembert functional equation satisfied by the shifted cost H derived from the J-cost. Researchers classifying solutions to the Recognition Composition Law cite it as the target property after the log-coordinate change. It consists of the normalization H(0)=1 together with the symmetric additive relation that follows from evenness and quadratic consistency.
claimA function $H : ℝ → ℝ$ satisfies the d'Alembert equation when $H(0) = 1$ and $H(t + u) + H(t - u) = 2 H(t) H(u)$ for all real $t, u$.
background
In the Recognition Science framework the J-cost obeys the Recognition Composition Law. The upstream definition from CostAlgebra sets $H(x) := J(x) + 1$, under which the law becomes exactly the d'Alembert relation $H(xy) + H(x/y) = 2 H(x) H(y)$. The module transforms an original cost functional $F$ on positive reals (symmetric, normalized at 1, with quadratic combiner) into an even function $G(t) = F(e^t)$ with $G(0) = 0$; the consistency condition then reduces to the stated form after the further shift $H = G + 1$.
proof idea
This is a direct definition. It packages the normalization condition at zero with the two-variable additive relation obtained after the shift from the J-cost and the evenness constraint on Φ.
why it matters in Recognition Science
The definition supplies the hypothesis for the classification theorem dAlembert_classification, which identifies the unique regular solution as cosh under the calibration $H''(0) = 1$. It closes the step from the Recognition Composition Law (T5) to the explicit functional form used downstream to derive evenness and vanishing first derivative at zero. The result anchors the transition from the phi-ladder construction to the eight-tick octave and spatial dimension D=3.
scope and limits
- Does not impose continuity or differentiability on H.
- Does not assert existence of non-constant solutions.
- Does not reconnect H to the original cost functional F.
- Does not restrict the domain beyond the reals.
formal statement (Lean)
107def IsDAlembertSolution (H : ℝ → ℝ) : Prop :=
proof body
Definition body.
108 H 0 = 1 ∧ ∀ t u, H (t + u) + H (t - u) = 2 * H t * H u
109
110/-- D'Alembert solutions are even. -/