dAlembert_classification
plain-language theorem explainer
Any continuous real-valued H with H(0)=1 obeying the d'Alembert equation H(t+u)+H(t-u)=2 H(t) H(u) is either the constant 1, cosh(αx) for some real α, or cos(αx) for some real α. Workers on the Recognition Composition Law and the J-automorphism classification cite the result to obtain explicit solution forms. The proof first lifts continuity to C^∞ regularity, derives the ODE H''=c H from the functional equation, then branches on the sign of c=H''(0) and invokes ODE uniqueness in each case.
Claim. Let $H:ℝ→ℝ$ be continuous, satisfy $H(0)=1$, and obey $H(t+u)+H(t-u)=2H(t)H(u)$ for all real $t,u$. Then either $H(x)=1$ for all $x$, or there exists $α∈ℝ$ such that $H(x)=cosh(αx)$ for all $x$, or there exists $α∈ℝ$ such that $H(x)=cos(αx)$ for all $x$.
background
In CostAlgebra the shifted cost is defined by $H(x)=J(x)+1=½(x+x^{-1})$, where J satisfies the Recognition Composition Law; under this shift the RCL becomes exactly the displayed d'Alembert equation. The module proves Aczél's smoothness theorem: every continuous solution with $H(0)=1$ is real-analytic (ContDiff ℝ ⊤). Upstream lemmas supply the two preparatory steps: dAlembert_contDiff_smooth converts continuity into infinite differentiability via integration bootstrap, while dAlembert_to_ODE_general extracts the second-order linear ODE $H''(t)=c·H(t)$ with constant $c=H''(0)$.
proof idea
The tactic proof first applies dAlembert_contDiff_smooth to obtain ContDiff ℝ ⊤ H, then reduces to C² and differentiable. It sets $c:=H''(0)$ and invokes dAlembert_to_ODE_general to secure the ODE. Case split on the sign of c: when $c>0$ a rescaled $g$ satisfies $g''=g$ and ode_cosh_uniqueness_contdiff yields the cosh form; when $c<0$ the ODE becomes $g''=-g$ and ode_cos_uniqueness produces the cosine; when $c=0$ is_const_of_deriv_eq_zero forces the constant solution.
why it matters
The classification is the central step of the Aczél–Kannappan theorem inside the Recognition Science cost layer and is invoked by dAlembert_contDiff_top to reach ContDiff ℝ ⊤, by FourthGate.dAlembert_classification, and by GeneralizedDAlembert.aczel_kannappan_continuous_dAlembert. It supplies the explicit solution forms required to connect the Recognition Composition Law to J-uniqueness (T5) and the self-similar fixed point phi (T6) in the forcing chain T0–T8. The result also calibrates the eight-tick octave and the D=3 spatial dimension that follow from the same functional equation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.