aczel_kernel_ode
plain-language theorem explainer
The theorem extracts the ODE property from the Aczel regularity kernel for any H satisfying the d'Alembert equation once the smoothness package is assumed. Researchers tracing the d'Alembert forcing chain toward T5 J-uniqueness in Recognition Science cite it to obtain the calibrated second-derivative condition H'' = H. The proof is a direct term projection of the ode field from aczelRegularityKernel H.
Claim. Assuming the Aczél smoothness package, for any function $H : ℝ → ℝ$ the d'Alembert-to-ODE hypothesis holds: continuous solutions of the d'Alembert equation with $H(0)=1$ satisfy the ODE $H''=H$.
background
The Aczel Classification Package supplies the smoothness and ODE kernel for the d'Alembert segment of the forcing chain. The shifted cost is defined by $H(x) = J(x) + 1 = ½(x + x^{-1})$, converting the Recognition Composition Law into the standard d'Alembert equation $H(xy) + H(x/y) = 2 H(x) H(y)$. The AczelSmoothnessPackage states that any continuous solution of $H(t+u) + H(t-u) = 2 H(t) H(u)$ with $H(0)=1$ is $C^∞$. The aczelRegularityKernel packages both the smoothness result and the ODE property derived from it. This module lets downstream exclusivity code depend on the kernel without invoking the raw Aczel axiom.
proof idea
The proof is a one-line wrapper that applies the ode field of aczelRegularityKernel H.
why it matters
This supplies the canonical public T5 input bundle for the primitive-to-uniqueness route. It records the step in which continuous d'Alembert solutions yield the calibrated ODE kernel $H''=H$, feeding the J-uniqueness claim in the forcing chain. The module doc notes that downstream code can now depend on this kernel without touching the raw Aczel axiom directly.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.