dAlembert_classification
plain-language theorem explainer
The theorem asserts that any continuous H satisfying the d'Alembert equation H(t+u)+H(t-u)=2H(t)H(u) with H(0)=1 and H''(0)=1 must equal cosh(t). Researchers deriving the explicit form of the J-cost from the Recognition Composition Law cite it to select the hyperbolic branch under unit calibration. The proof is a one-line wrapper that applies dAlembert_cosh_solution after unpacking the IsDAlembertSolution hypothesis into its base equation and continuity components.
Claim. Let $H : ℝ → ℝ$ satisfy $H(0)=1$ and $H(t+u)+H(t-u)=2H(t)H(u)$ for all real $t,u$, be continuous, and obey $H''(0)=1$. Under the regularity hypotheses that continuous solutions are smooth and satisfy the associated ODE and bootstrap conditions, $H(t)=cosh(t)$ for all real $t$.
background
The shifted cost is defined by $H(x)=J(x)+1$, where $J$ satisfies the Recognition Composition Law $J(xy)+J(x/y)=2J(x)J(y)+2J(x)+2J(y)$. In logarithmic coordinates $G(t)=F(exp(t))$ the even function $G$ with $G(0)=0$ obeys the additive d'Alembert equation $G(t+u)+G(t-u)=Φ(G(t),G(u))$. The module shows that continuity plus the calibration $G''(0)=1$ forces the unique solution $G(t)=cosh(t)$, which recovers the hyperbolic form for the original cost. The upstream Aczél–Kannappan result states that continuous solutions are constant, cosine, or cosh; the calibration selects the cosh case.
proof idea
The proof is a one-line wrapper that invokes dAlembert_cosh_solution, passing the base equation and functional equation extracted from the two components of IsDAlembertSolution, together with continuity, the calibration deriv(deriv H) 0 = 1, and the four regularity hypotheses on smoothness, ODE derivation, continuity, differentiability, and linear bootstrap.
why it matters
This result supplies the unique hyperbolic solution required by the forcing chain at T5 J-uniqueness, where $J(x)=cosh(log x)-1$. It feeds the Aczél proof module, the Fourth Gate, and the generalized d'Alembert theorems in GeneralizedDAlembert, confirming that the Recognition Composition Law admits only the d'Alembert form under the stated regularity and thereby fixing the explicit cosh expression used in mass formulas and the phi-ladder.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.