AczelRegularityKernel
plain-language theorem explainer
The regularity kernel structure packages the two hypotheses that convert a continuous d'Alembert solution into the unique J-cost kernel. Workers on the T5 uniqueness step in the Recognition forcing chain cite it as the explicit interface to the Aczel classification package. The declaration is a bare structure that simply bundles the smoothness implication and the ODE reduction imported from the FunctionalEquation module.
Claim. Let $H : ℝ → ℝ$. The regularity kernel condition on $H$ holds when $H$ satisfies both the implication that continuity in the d'Alembert equation yields smoothness and the reduction of that equation to the ODE $H'' = H$.
background
In Recognition Science the shifted cost is defined by $H(x) = J(x) + 1 = ½(x + x^{-1})$, where $J$ is the J-cost. Under this substitution the Recognition Composition Law reduces to the d'Alembert equation $H(xy) + H(x/y) = 2 H(x) H(y)$. The Aczel Classification module isolates the consequences of this equation: continuous solutions are smooth and smoothness yields the calibrated ODE $H'' = H$ (quoted from the module doc: “continuous d'Alembert solutions are smooth; once smoothness is available, the calibrated ODE kernel $H'' = H$ follows”).
proof idea
The declaration is a structure definition whose two fields directly reference the imported hypotheses dAlembert_continuous_implies_smooth_hypothesis H and dAlembert_to_ODE_hypothesis H. No tactics or reductions are applied; the structure merely records these two propositions as its fields.
why it matters
The structure supplies the regularity bridge used by the public T5 theorem primitive_to_uniqueness_of_kernel, which takes PrimitiveCostHypotheses F together with the kernel condition on H F and concludes that F coincides with Jcost on positive reals. It thereby isolates the Aczel seam for the J-uniqueness step (T5) in the T0–T8 forcing chain without exposing the raw classification axiom to downstream code. The same structure appears in the PublicCostLayer of the dimensional-constraints rebuttal.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.