H_AczelClassification
plain-language theorem explainer
The Aczél classification statement asserts that every continuous real function H with H(0)=1 obeying the d'Alembert equation H(t+u)+H(t-u)=2 H(t) H(u) is infinitely differentiable. Recognition Science cost models cite this to upgrade the shifted cost function to C^∞. The definition is discharged by a separate theorem that applies the integration bootstrap from continuity through repeated differentiation.
Claim. Every continuous function $H:ℝ→ℝ$ satisfying $H(0)=1$ and $H(t+u)+H(t-u)=2H(t)H(u)$ for all real $t,u$ is of class $C^∞$.
background
The shifted cost is defined by H(x)=J(x)+1 where J(x)=(x+x^{-1})/2 satisfies the Recognition Composition Law; under this change the RCL becomes the d'Alembert equation H(xy)+H(x/y)=2 H(x) H(y). The module states that every continuous solution of the additive form with H(0)=1 is C^∞ and lists the three solutions: the constant 1, cosh(λt), and cos(λt). Upstream CostAlgebra.H records exactly this reparametrization: “The shifted cost: H(x) = J(x) + 1 = ½(x + x⁻¹). Under H, the RCL becomes the standard d'Alembert equation.”
proof idea
The declaration is the definition of the universal proposition. Its validity is established downstream by h_aczel_classification_proved, which applies the theorem dAlembert_contDiff_top obtained from the integration bootstrap (representation formula, repeated differentiation, ODE derivation).
why it matters
This definition supplies the statement proved unconditionally in h_aczel_classification_proved, removing the last foundation axiom from the IndisputableMonolith codebase. It is invoked by dAlembert_contDiff_top to complete the Aczél classification. The result confirms smoothness of the cost-derived H, consistent with J-uniqueness in the forcing chain (T5).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.