IndisputableMonolith.Cost.AczelProof
The module proves the Aczél–Kannappan classification for continuous solutions of the d'Alembert equation H(t+u) + H(t-u) = 2 H(t) H(u) with H(0)=1. Researchers tracing the T5 J-uniqueness step in the Recognition forcing chain cite it to obtain the trichotomy of constant, cosh, and cos forms. The argument upgrades continuity to C^∞ via the smoothness bootstrap then reduces the equation to an ODE whose solutions are matched case-by-case.
claimEvery continuous function $H:ℝ→ℝ$ with $H(0)=1$ satisfying $H(t+u)+H(t-u)=2H(t)H(u)$ for all real $t,u$ equals the constant 1, $cosh(α·)$ for some $α∈ℝ$, or $cos(α·)$ for some $α∈ℝ$.
background
This module belongs to the Cost domain and supplies the explicit classification required for the d'Alembert segment of the T5 forcing chain. It imports the AczelClass typeclass that carries the smoothness package, the AczelTheorem stating that every continuous solution is C^∞, and FunctionalEquation helpers for the J-cost uniqueness argument. The d'Alembert equation itself arises from the Recognition Composition Law applied to the J-cost function J(x)=(x+x^{-1})/2-1.
proof idea
The module first invokes the integration bootstrap dAlembert_contDiff_smooth to obtain C^∞ regularity from continuity. It then applies dAlembert_to_ODE_general to extract the second-order linear ODE H''=cH with c=H''(0) from the C² case of the functional equation. ODE uniqueness on each branch of the trichotomy for c yields the three explicit solution families.
why it matters in Recognition Science
The module supplies the classification that AczelClassification packages for the d'Alembert forcing chain and that GeneralizedDAlembert uses to relax the polynomial-degree bound in the Translation Theorem. It completes the smoothness-plus-ODE step needed for T5 J-uniqueness inside the Recognition Science framework.
scope and limits
- Does not classify solutions lacking continuity.
- Does not treat the equation on domains other than the reals.
- Does not derive the constant c from the J-cost definition.
- Does not address stability under small perturbations.
used by (2)
depends on (3)
declarations in this module (16)
-
abbrev
smooth -
def
Phi -
lemma
phi_zero -
lemma
phi_hasDerivAt -
lemma
phi_differentiable -
lemma
deriv_phi_eq -
lemma
exists_integral_ne_zero -
lemma
representation_formula -
lemma
phi_contDiff_succ -
theorem
dAlembert_contDiff_nat -
theorem
dAlembert_contDiff_smooth -
theorem
dAlembert_to_ODE_general -
theorem
ode_neg_zero_uniqueness -
theorem
ode_cos_uniqueness -
theorem
dAlembert_classification -
theorem
dAlembert_contDiff_top