ode_regularity_differentiable_of_smooth
plain-language theorem explainer
Any infinitely differentiable real-valued function H satisfies the regularity hypothesis that continuous solutions to the linear ODE f'' = f are differentiable. Researchers closing uniqueness arguments for the Recognition cost kernel via Aczél methods cite this result to discharge the differentiable leg of the bootstrap. The argument is a direct term that extracts first-order differentiability from the C^∞ assumption without using the ODE or continuity premises.
Claim. If $H : ℝ → ℝ$ is $C^∞$, then $(∀ t, H''(t) = H(t)) → (H$ continuous$) → (H$ differentiable$)$.
background
The module isolates Aczél-dependent closure theorems for the cost functional equation, separate from the axiom-free core. The shifted cost H is defined by H(x) = J(x) + 1, where J satisfies the Recognition Composition Law and converts it to the d'Alembert equation H(xy) + H(x/y) = 2 H(x) H(y). Upstream, ode_regularity_differentiable_hypothesis asserts that pointwise satisfaction of f'' = f together with continuity implies differentiability; the companion ode_linear_regularity_bootstrap_hypothesis lifts this to C².
proof idea
Term-mode one-liner. The construction ignores the ODE equality and continuity assumptions, reduces ContDiff ℝ ⊤ to ContDiff ℝ 1 via of_le le_top, then invokes the differentiable method with a decide tactic confirming the order is nonzero.
why it matters
It supplies the differentiable regularity bridge used by primitive_to_uniqueness_of_kernel, the public T5 statement that extracts J-uniqueness from PrimitiveCostHypotheses plus an AczelRegularityKernel. The result sits inside the cost-domain bootstrap that supports the J-uniqueness step (T5) of the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.