H_AczelClassification
plain-language theorem explainer
Every continuous real-valued function H obeying H(0)=1 and the d'Alembert equation H(t+u)+H(t-u)=2 H(t) H(u) is infinitely differentiable. Workers on functional equations or the Recognition Science cost algebra cite this result to remove the last foundation axiom. The proof is an integration bootstrap that upgrades continuity to C^1 via an antiderivative representation, then iterates to C^∞.
Claim. Let $H:ℝ→ℝ$ satisfy $H(0)=1$, be continuous, and obey $H(t+u)+H(t-u)=2H(t)H(u)$ for all real $t,u$. Then $H$ is $C^∞$.
background
The shifted cost function is defined by H(x)=J(x)+1 where J is the Recognition cost; under this substitution the Recognition Composition Law becomes the d'Alembert equation H(xy)+H(x/y)=2 H(x) H(y). The module reparametrizes to H_F(t)=G_F(t)+1 for convenience in the functional-equation setting. The local theoretical setting is the Aczél smoothness theorem for continuous solutions of this equation with H(0)=1, which classifies them as 1, cosh(λt), or cos(λt), all of which are C^∞.
proof idea
This declaration is the definition of the Aczél classification property. The actual proof that the property holds is supplied by the downstream theorem dAlembert_contDiff_top, which first obtains a representation formula H(t)=(Φ(t+δ)−Φ(t−δ))/(2 Φ(δ)) from the functional equation and the fundamental theorem of calculus, then bootstraps regularity from continuous to C^1 to C^2 and finally to C^∞.
why it matters
This definition was the sole remaining foundation axiom in the IndisputableMonolith codebase; its proof eliminates that axiom. It is invoked directly by dAlembert_contDiff_top and by the unconditional theorem h_aczel_classification_proved. The result closes the integration-bootstrap step that converts the Recognition Composition Law into the classical Aczél classification, confirming that all continuous solutions are C^∞ and thereby supporting the ODE derivation H''=c H used downstream for the cosh/cos classification.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.