IndisputableMonolith.Cost.AczelProof
The AczelProof module establishes the Aczél–Kannappan classification of continuous solutions to the d'Alembert functional equation. Researchers on the T5 J-uniqueness and generalized d'Alembert arguments cite it for the required smoothness step. The argument upgrades continuity to C^∞ by integration bootstrap, reduces the equation to an ODE via the curvature constant at zero, and recovers the explicit forms by case analysis on that constant.
claimAny continuous $H : ℝ → ℝ$ with $H(0) = 1$ satisfying $H(t+u) + H(t-u) = 2 H(t) H(u)$ for all real $t,u$ equals the constant function 1, or $H(t) = cosh(α t)$, or $H(t) = cos(α t)$ for some real α.
background
The module operates inside the Cost domain and supplies the concrete instances for the d'Alembert smoothness package declared as a typeclass in the imported AczelClass. The upstream AczelTheorem asserts that every continuous solution of $H(t+u) + H(t-u) = 2 H(t) H(u)$ with $H(0) = 1$ is C^∞. It also draws on FunctionalEquation lemmas that support the T5 cost uniqueness proof. The local setting is the Recognition Science forcing chain in which this functional equation appears during derivation of the J-cost function.
proof idea
The module structures the classification around the AczelSmoothnessPackage class. It first applies the integration bootstrap dAlembert_contDiff_smooth to lift continuity to C^∞. It then invokes dAlembert_to_ODE_general to obtain the ODE H'' = c H with c = H''(0). The final stage solves the ODE by trichotomy on the sign of c, using uniqueness in each branch to recover the constant, hyperbolic, and trigonometric solutions.
why it matters in Recognition Science
This module completes the smoothness and classification step required for the d'Alembert component of the Recognition Science forcing chain. It feeds the AczelClassification package, which packages the continuous-to-smooth transition together with the calibrated ODE kernel. It also supports GeneralizedDAlembert by discharging polynomial regularity assumptions in the Translation Theorem. The result aligns with the 1966 Aczél classification and supplies the cosh form that matches the explicit expression for J in the T5 uniqueness argument.
scope and limits
- Does not classify solutions that lack continuity.
- Does not derive the parameter α from Recognition Science constants.
- Does not extend the classification beyond real-valued functions on the reals.
- Does not treat stability under perturbation of the functional equation.
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