h_aczel_classification_proved
plain-language theorem explainer
The theorem establishes that every continuous real function H satisfying H(0)=1 and the d'Alembert equation H(t+u)+H(t-u)=2 H(t) H(u) is infinitely differentiable. Researchers applying the Recognition Science cost model cite it to discharge the final foundational hypothesis. The proof is a direct one-line application of the classification theorem that maps the equation to the known C^∞ cases of the constant, cosh, and cos functions.
Claim. Let $H:ℝ→ℝ$. If $H(0)=1$, $H$ is continuous, and $H(t+u)+H(t-u)=2H(t)H(u)$ for all real $t,u$, then $H$ belongs to $C^∞(ℝ)$.
background
The shifted cost function is defined by $H(x)=J(x)+1$, where $J$ is the cost from the Recognition Composition Law; under this shift the law reduces exactly to the d'Alembert equation. The module treats the Aczél classification as the statement that any continuous solution with $H(0)=1$ is $C^∞$, and the upstream smoothness package supplies the interface that any such solution is infinitely differentiable. The local setting is the integration-bootstrap argument: continuity plus the functional equation yields an antiderivative representation that bootstraps regularity to all orders, after which the ODE $H''=cH$ classifies the solutions.
proof idea
The declaration is a one-line wrapper that applies dAlembert_contDiff_top to the four hypotheses. That theorem first invokes the classification into the three cases (constant, cosh, cos), then verifies that each case is $C^∞$ by direct differentiation or by casting the infinite differentiability of the hyperbolic and trigonometric functions.
why it matters
The result removes the sole remaining foundation axiom H_AczelClassification from the IndisputableMonolith codebase, completing the unconditional proof that continuous d'Alembert solutions are smooth. It closes the last gap before the J-uniqueness step (T5) and the forcing chain that derives the phi-ladder and the eight-tick octave. Downstream cost-algebra results that previously carried the hypothesis as an assumption now inherit a fully proved statement.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.