aczel_kannappan_continuous_dAlembert
plain-language theorem explainer
The Aczél–Kannappan classification states that every continuous real-valued function H with H(0) = 1 obeying the d'Alembert equation H(x + y) + H(x - y) = 2 H(x) H(y) for all real x and y is either the constant function 1, a hyperbolic cosine cosh(α x), or a trigonometric cosine cos(α x). Recognition Science researchers cite this result to replace the polynomial-degree-≤-2 hypothesis on the combiner in the Translation Theorem with the weaker assumption of continuity. The proof is a one-line wrapper that invokes the pre-established dAlembert分类已证
Claim. Let $H : ℝ → ℝ$ be continuous with $H(0) = 1$. Suppose $H(x + y) + H(x - y) = 2 H(x) H(y)$ holds for all real $x, y$. 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 Recognition Science the shifted cost is defined by $H(x) = J(x) + 1$, where $J$ is the unique solution of the Recognition Composition Law $J(xy) + J(x/y) = 2 J(x) J(y) + 2 J(x) + 2 J(y)$. Under this reparametrization the RCL reduces exactly to the classical d'Alembert equation $H(x + y) + H(x - y) = 2 H(x) H(y)$. The module GeneralizedDAlembert carries out Move 3 of the foundation by showing that continuity of the combiner suffices once the Aczél–Kannappan trichotomy is available, thereby discharging the stronger polynomial restriction of the original Translation Theorem.
proof idea
The proof is a one-line wrapper that applies the theorem dAlembert_classification from IndisputableMonolith.Cost.FunctionalEquation to the four hypotheses H, h_one, hCont and hEq.
why it matters
This theorem supplies the continuous-case classification required by AxiomDischargePlan.aczel_kannappan_via_cases and AxiomDischargePlan.cosh_rescaling_lemma; it is also invoked inside the same module by laws_continuous_subsumes_polynomial and log_bilinear_affine_lift_classification. By establishing the trichotomy under continuity alone it removes the polynomial-degree-≤-2 hypothesis from the Translation Theorem, consistent with the framework's reduction of physics to the single functional equation via the forcing chain T0–T8 and the Recognition Composition Law. The result closes one scaffolding step in the discharge plan while leaving open whether continuity itself can be weakened further.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.