IsDAlembertSolution
plain-language theorem explainer
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.
Claim. A 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
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.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.