aczelRegularityKernel
plain-language theorem explainer
The declaration supplies the default regularity kernel for a function H satisfying the d'Alembert equation once the Aczel smoothness package is assumed. Workers on the T5 J-uniqueness step cite it to obtain both infinite differentiability and the calibrated ODE H'' = H without direct appeal to the raw classification axiom. The definition assembles the kernel structure by invoking the smoothness theorem on the continuous case and reducing to the ODE lemma.
Claim. Given the Aczel smoothness package, the default regularity kernel for a map $H:ℝ→ℝ$ is the structure whose smoothness component asserts that every continuous solution of the d'Alembert equation $H(t+u)+H(t-u)=2H(t)H(u)$ with $H(0)=1$ is $C^∞$, and whose ODE component asserts that the same equation plus $H''=H$ follows from the calibrated second-derivative condition.
background
The Aczel Classification module packages the d'Alembert segment of the forcing chain so that continuity plus the functional equation automatically yields smoothness. The shifted cost function is defined by $H(x)=J(x)+1$, converting the Recognition Composition Law into the standard d'Alembert form $H(xy)+H(x/y)=2H(x)H(y)$. The upstream AczelSmoothnessPackage states that any continuous solution of $H(t+u)+H(t-u)=2H(t)H(u)$ with $H(0)=1$ is infinitely differentiable, citing the complete classification into the constant solution and the hyperbolic-cosine family.
proof idea
The definition constructs the AczelRegularityKernel structure directly. The smooth field is filled by the projection dAlembert_smooth_of_aczel H. The ode field is obtained by first deriving ContDiff ℝ ⊤ H from dAlembert_smooth_of_aczel under the hypotheses h_one, h_cont, h_dAlembert, then feeding the resulting smoothness into dAlembert_to_ODE_theorem together with h_d2_zero.
why it matters
This kernel supplies the regularity interface required by primitive_to_uniqueness_aczel, which concludes that any primitive cost hypothesis recovers the J-cost function. It therefore closes the seam between the Aczel classification and the T5 uniqueness step in the T0-T8 forcing chain. The two convenience projections aczel_kernel_smooth and aczel_kernel_ode extract the smooth and ode components for downstream use without exposing the underlying Aczel axiom.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.