aczel_kernel_ode
The theorem projects the ODE property H'' = H from the Aczel regularity kernel for any H obeying the d'Alembert equation once the smoothness package is assumed. Recognition Science researchers working on the T5 J-uniqueness step cite it to obtain the calibrated differential kernel without re-proving differentiability. The proof is a direct one-line projection of the ode field from the aczelRegularityKernel instance.
claimAssuming the Aczél smoothness package, for any function $H : ℝ → ℝ$ the d'Alembert-to-ODE hypothesis holds, i.e., the second derivative satisfies $H'' = H$ once $H(0) = 1$, continuity, and the equation $H(t+u) + H(t-u) = 2 H(t) H(u)$ are given.
background
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 every continuous solution of $H(t+u) + H(t-u) = 2 H(t) H(u)$ with $H(0)=1$ is $C^∞$. The aczelRegularityKernel then packages both the smoothness result and the derived ODE relation into a single structure.
proof idea
The proof is a one-line wrapper that extracts the ode field of the aczelRegularityKernel H instance under the AczelSmoothnessPackage.
why it matters in Recognition Science
This supplies the canonical public T5 input bundle for the primitive-to-uniqueness route in the forcing chain, allowing downstream code to depend on the calibrated ODE kernel without touching the raw Aczel axiom. It completes the smoothness-to-ODE step inside the Aczel classification package and supports the transition from functional equation to differential equation required for J-uniqueness.
scope and limits
- Does not prove the Aczel smoothness property itself.
- Does not apply without the AczelSmoothnessPackage instance.
- Does not derive explicit solution forms such as cosh.
- Does not extend to non-continuous or non-real cases.
formal statement (Lean)
43theorem aczel_kernel_ode [AczelSmoothnessPackage] (H : ℝ → ℝ) :
44 dAlembert_to_ODE_hypothesis H :=
proof body
Term-mode proof.
45 (aczelRegularityKernel H).ode
46
47/-- Canonical public T5 input bundle.
48
49This is the primitive-to-uniqueness route exposed to the rest of the public RS
50surface. `JensenSketch` remains available as a compatibility layer, but the
51official statement now records the reciprocal-cost, normalization, composition,
52calibration, and continuity assumptions explicitly. -/