smooth
plain-language theorem explainer
The private abbreviation smooth assigns the top element of the extended naturals to represent C^∞ regularity. Researchers applying Aczél's classification to d'Alembert equations in cost functional equations cite this constant when invoking the full bootstrap from continuity. It appears as a direct one-line assignment of ⊤ in WithTop ℕ∞ to mark infinite differentiability for H.
Claim. Let $smooth := top$ in the extended naturals $WithTop ℕ_∞$, denoting the $C^∞$ class for any continuous solution $H$ of the d'Alembert equation $H(t+u) + H(t-u) = 2 H(t) H(u)$ with $H(0)=1$.
background
The module establishes that every continuous solution of the d'Alembert functional equation with H(0)=1 is C^∞, via integration bootstrap: a representation formula H(t) = (Φ(t+δ) − Φ(t−δ))/(2 Φ(δ)) from FTC, followed by iterated regularity lifting from C^0 to C^1 to C^∞. Upstream results supply the identical top assignment in AczelProof under the comment Phase 1: Integration Bootstrap. This removes the prior H_AczelClassification axiom in the IndisputableMonolith cost layer.
proof idea
One-line definition that directly sets the identifier smooth to the top element (⊤ : ℕ∞) of WithTop ℕ∞.
why it matters
This constant populates the AczelRegularityKernel structure that feeds primitive_to_uniqueness_of_kernel, which derives F x = Cost.Jcost x from PrimitiveCostHypotheses. It closes the regularity seam for T5 J-uniqueness in the forcing chain and supports downstream uses in standardLagrangian and alphaInv_linear_rate. The module doc states this completes the zero-sorry proof of Aczél's 1966 classification.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.