aczel_kernel_ode
plain-language theorem explainer
Under the Aczél smoothness package the shifted cost function satisfies the second-order ODE extracted from the d'Alembert equation. Researchers assembling the T5 uniqueness step in the forcing chain cite this projection when they need the calibrated kernel without invoking the raw Aczél axiom. The proof is a one-line field projection from the regularity kernel construction.
Claim. Assuming the Aczél smoothness package, for any $H:ℝ→ℝ$ the hypothesis that $H$ satisfies the ODE $H''=H$ (with the d'Alembert equation, $H(0)=1$, and continuity) holds.
background
The module packages the portion of the d'Alembert forcing chain supplied by the Aczél classification theorem: continuous solutions are smooth, and smoothness yields the calibrated ODE kernel. The shifted cost is defined by $H(x)=J(x)+1=½(x+x^{-1})$, which converts the recognition composition law into the standard d'Alembert equation $H(xy)+H(x/y)=2H(x)H(y)$. The Aczél smoothness package asserts that any continuous solution of $H(t+u)+H(t-u)=2H(t)H(u)$ with $H(0)=1$ is $C^∞$. The aczelRegularityKernel supplies the default kernel carrying both smoothness and the ODE.
proof idea
The proof is a one-line wrapper that applies aczelRegularityKernel to H and projects its ode field.
why it matters
This supplies the ODE kernel for the Aczél classification package inside the d'Alembert forcing chain. It supports the primitive-to-uniqueness route exposed on the public Recognition Science surface and fills the step from smoothness to the calibrated ODE $H''=H$, directly relevant to T5 J-uniqueness. The module doc states that downstream exclusivity code can now depend on this kernel without touching the raw Aczél axiom.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.