IndisputableMonolith.Cost.AczelProof
AczelProof module establishes the Aczél–Kannappan classification of continuous d'Alembert solutions within the Recognition Science cost framework. Researchers on T5 J-uniqueness and the translation theorem cite it for explicit forms after regularity is secured. The argument upgrades continuity to C^∞ via integration bootstrap, reduces the equation to the ODE H''=cH, and solves the trichotomy on c by uniqueness.
claimEvery continuous function $H:\mathbb{R}\to\mathbb{R}$ with $H(0)=1$ satisfying the d'Alembert equation $H(t+u)+H(t-u)=2H(t)H(u)$ equals the constant 1, $\cosh(\alpha t)$ for some $\alpha\in\mathbb{R}$, or $\cos(\alpha t)$ for some $\alpha\in\mathbb{R}$.
background
The module implements the classification proof in the Cost domain. It imports the smoothness typeclass interface from AczelClass, the statement that every continuous solution is C^∞ from AczelTheorem, and T5 functional-equation helpers from FunctionalEquation. The local setting is the normalized d'Alembert equation arising in the translation theorem for route-independence combiners P of polynomial degree at most two.
Key objects defined here include the smoothness predicate, the auxiliary function Phi, and the ODE reduction that extracts the constant c=H''(0).
proof idea
The module proceeds in three stages. The integration bootstrap dAlembert_contDiff_smooth upgrades continuity to C^∞. The reduction dAlembert_to_ODE_general then yields the linear ODE H''=cH. ODE uniqueness in each branch of the trichotomy on the sign of c produces the constant, hyperbolic, and trigonometric solutions.
why it matters in Recognition Science
This module feeds AczelClassification, which packages the smoothness and ODE kernel for the d'Alembert forcing chain, and GeneralizedDAlembert, which uses it to discharge the regularity requirement in the translation theorem. It supplies the explicit-solution step that closes the gap left by the quartic-log counterexample for higher-degree polynomials, supporting the T5 cost-uniqueness argument.
scope and limits
- Does not classify solutions lacking continuity.
- Does not treat the equation without the normalization H(0)=1.
- Does not extend to complex-valued or multi-variable cases.
- Does not supply bounds on the parameter alpha.
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