aczelRegularityKernel
plain-language theorem explainer
The definition builds the default regularity kernel for the shifted cost function H under the current Aczél smoothness package. Researchers tracing the d'Alembert segment of the forcing chain cite it to obtain both the continuity-to-smoothness implication and the ODE property without direct appeal to the classification axiom. It is realized by applying the package smoothness result to populate the first field and then invoking the ODE derivation lemma on the resulting differentiability.
Claim. Let $H : ℝ → ℝ$. Under the Aczél smoothness package the regularity kernel for $H$ is the structure whose first component asserts that continuity plus the d'Alembert equation $H(t+u)+H(t-u)=2H(t)H(u)$ with $H(0)=1$ imply $H$ is $C^∞$, and whose second component asserts that the same hypotheses plus $H''(0)=0$ yield the ODE $H''=H$.
background
The AczelRegularityKernel structure packages two hypotheses for a function $H$: the implication from continuity to infinite differentiability under the d'Alembert equation, and the ODE hypothesis that follows once differentiability is granted. The shifted cost $H(x)=J(x)+1$ converts the Recognition Composition Law into the standard d'Alembert form $H(xy)+H(x/y)=2H(x)H(y)$. The AczelSmoothnessPackage class encodes the 1966 classification result that every continuous solution with $H(0)=1$ is of the form constant or $cosh(λt)$ and hence $C^∞$.
proof idea
The definition is a one-line structure constructor. It sets the smoothness field by direct application of dAlembert_smooth_of_aczel to $H$. The ODE field is obtained by first calling that same smoothness lemma to produce a ContDiff hypothesis, then feeding the result together with the d'Alembert and second-derivative-zero assumptions into dAlembert_to_ODE_theorem.
why it matters
It supplies the canonical T5 input bundle used by primitive_to_uniqueness_aczel, which in turn feeds the exclusivity argument for the J-uniqueness step in the forcing chain. The module doc states that downstream code can now depend on this kernel without touching the raw Aczel axiom. The construction therefore closes the seam between the Aczél classification and the calibrated ODE required for the eight-tick octave and spatial-dimension steps.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.