IndisputableMonolith.Cost.AczelProof
AczelProof supplies the Aczél–Kannappan classification of continuous solutions to the d'Alembert equation H(t+u) + H(t-u) = 2 H(t) H(u) with H(0)=1. Researchers tracing the Recognition Science T5 J-uniqueness chain cite it to obtain the explicit cosh and cos forms after smoothness is established. The argument upgrades continuity to C^∞ via integration bootstrap then reduces to the ODE H'' = c H whose solutions are classified by the sign of c.
claimAny continuous $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, or $cosh(α t)$ for some $α∈ℝ$, or $cos(α t)$ for some $α∈ℝ$.
background
The module implements the classification theorem inside the Recognition Science cost analysis that derives T5 J-uniqueness from the Recognition Composition Law. It imports the AczelSmoothnessPackage typeclass from AczelClass, whose bootstrap theorem states that every continuous solution is C^∞. Supporting lemmas come from FunctionalEquation, while AczelTheorem records the fully proved smoothness statement. The local setting is the forcing chain T0–T8 where the d'Alembert equation encodes the self-similar fixed point phi.
proof idea
The module first applies the integration bootstrap dAlembert_contDiff_smooth to reach C^∞ from continuity. It then invokes dAlembert_to_ODE_general to obtain the second-order equation H'' = c H with c = H''(0). ODE uniqueness on each branch of the trichotomy for c produces the three explicit solutions.
why it matters in Recognition Science
This module feeds the AczelClassification package, which supplies the smoothness and calibrated ODE kernel H''=H required by GeneralizedDAlembert to discharge the polynomial-regularity hypothesis in the Translation Theorem. It completes the d'Alembert step of the T5 forcing chain, enabling the phi-ladder mass formula and the eight-tick octave analysis.
scope and limits
- Does not classify solutions lacking the continuity hypothesis.
- Does not treat the equation on domains other than the reals.
- Does not address stability under small perturbations.
- Does not supply numerical or computational implementations.
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