H_AczelClassification
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^∞.
claimLet $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 in Recognition Science
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.
scope and limits
- Does not derive the explicit solution forms 1, cosh, or cos.
- Does not address measurability or other regularity weaker than continuity.
- Does not extend the result to complex or vector-valued functions.
- Does not quantify the constants λ appearing in the classified solutions.
Lean usage
theorem h_aczel_classification_proved : H_AczelClassification := fun H h_one h_cont h_dAlembert => dAlembert_contDiff_top H h_one h_cont h_dAlembertformal statement (Lean)
82def H_AczelClassification : Prop :=
proof body
Definition body.
83 ∀ (H : ℝ → ℝ),
84 H 0 = 1 →
85 Continuous H →
86 (∀ t u, H (t + u) + H (t - u) = 2 * H t * H u) →
87 ContDiff ℝ ⊤ H
88
89/-! ## §3 Integration Bootstrap: Continuous → C^∞ -/
90
91noncomputable section
92