aczelRegularityKernel
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.
claimGiven 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 in Recognition Science
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.
scope and limits
- Does not establish the Aczel smoothness package itself.
- Does not apply to functions that fail the d'Alembert equation.
- Does not produce explicit closed-form solutions beyond the kernel properties.
- Does not address non-real or discrete domains.
formal statement (Lean)
28noncomputable def aczelRegularityKernel [AczelSmoothnessPackage] (H : ℝ → ℝ) :
29 AczelRegularityKernel H where
30 smooth := dAlembert_smooth_of_aczel H
proof body
Definition body.
31 ode := by
32 intro h_one h_cont h_dAlembert h_d2_zero
33 have h_smooth : ContDiff ℝ ⊤ H :=
34 dAlembert_smooth_of_aczel H h_one h_cont h_dAlembert
35 exact dAlembert_to_ODE_theorem H h_smooth h_dAlembert h_d2_zero
36
37/-- Convenience projection: the smoothness theorem exported by the kernel. -/