dAlembert_classification
plain-language theorem explainer
The d'Alembert classification theorem states that any C² function H satisfying the d'Alembert functional equation with H(0)=1, H'(0)=0 and H''(0)=λ² must equal cosh(λt). Researchers verifying hyperbolic solutions in the Recognition Science cost algebra or functional-equation derivations would cite it. The proof splits on whether λ vanishes, reduces the nonzero case to the unit-calibration ODE uniqueness result via rescaling, and invokes the ODE uniqueness lemma for the scaled function.
Claim. Let $H : ℝ → ℝ$ be twice continuously differentiable. Suppose $H$ satisfies the d'Alembert equation $H(t+u) + H(t-u) = 2 H(t) H(u)$ for all real $t, u$, with $H(0) = 1$, $H'(0) = 0$, and $H''(0) = λ²$. Then $H(t) = cosh(λ t)$ for every real $t$.
background
SatisfiesDAlembert H encodes the d'Alembert structure: H(0)=1 together with the functional equation H(t+u) + H(t-u) = 2 H(t) H(u) for all t,u. This module presents the Fourth Gate as a derived cross-check on the curvature gate, where the normalized ODE G'' = G + 1 already selects the hyperbolic branch; the shifted lift H = G + 1 therefore satisfies d'Alembert automatically. Upstream, dalembert_deriv_ode supplies the relation H''(x) = H''(0) H(x), while ode_cosh_uniqueness_contdiff from Cost.FunctionalEquation establishes that the only C² solution to K'' = K with K(0)=1 and K'(0)=0 is cosh.
proof idea
The proof first obtains the second-order ODE H''(x) = λ² H(x) from dalembert_deriv_ode. It cases on λ = 0. When λ vanishes the ODE collapses to H'' = 0; combined with the initial conditions this forces H constant and equal to 1, matching cosh(0). For λ ≠ 0 the auxiliary K(s) := H(s/λ) is introduced; direct verification shows K satisfies K'' = K, K(0)=1, K'(0)=0 and C² regularity. The uniqueness lemma ode_cosh_uniqueness_contdiff then yields K(s) = cosh(s), which rescales to the claimed form for H.
why it matters
This supplies the general-λ version of the d'Alembert classification that feeds the AczelProof and GeneralizedDAlembert modules. It closes the scaling argument noted in the module documentation, confirming that the λ=1 case proved separately in dAlembert_with_unit_calibration extends to arbitrary λ. Within the Recognition Science framework it corroborates the T5 J-uniqueness step that produces the hyperbolic cosine as the unique self-similar solution compatible with the Recognition Composition Law. The declaration is not required for the main forcing chain T0-T8, which uses only the unit-calibration instance.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.