ode_regularity_bootstrap_of_smooth
plain-language theorem explainer
Any infinitely differentiable real-valued function H satisfies the regularity bootstrap hypothesis for the linear ODE f'' = f, so that pointwise satisfaction of the equation plus continuity and differentiability imply C² smoothness. Researchers closing uniqueness arguments for the d'Alembert equation under Aczél conditions cite this result to discharge regularity requirements. The proof is a one-line wrapper that downgrades the infinite differentiability assumption directly to the needed C² conclusion.
Claim. Let $H : ℝ → ℝ$ be infinitely differentiable. Then $H$ satisfies the regularity bootstrap hypothesis for the ODE $f'' = f$: whenever the second derivative of $H$ equals $H$ pointwise, $H$ is continuous, and $H$ is differentiable, it follows that $H$ is twice continuously differentiable.
background
The shifted cost is defined by $H(x) = J(x) + 1 = ½(x + x^{-1})$, where $J$ satisfies the Recognition Composition Law; under this reparametrization the law becomes the d'Alembert equation $H(xy) + H(x/y) = 2 H(x) H(y)$. The module isolates legacy Aczél-dependent closure theorems as a compatibility layer for callers that still require the Aczél axiom rather than the axiom-free core in the FunctionalEquation module. Upstream, dAlembert_cosh_solution states that a continuous solution with $H(0) = 1$ and second derivative 1 at zero must equal cosh, while ode_linear_regularity_bootstrap_hypothesis encodes the standard fact that linear ODEs with smooth coefficients have smooth solutions.
proof idea
This is a one-line wrapper. The infinite differentiability assumption is applied via the of_le le_top operation, which immediately yields the C² conclusion required by the bootstrap hypothesis regardless of the antecedent conditions on the ODE.
why it matters
The result closes a regularity seam in the Aczél-based route to T5 J-uniqueness. It is invoked by primitive_to_uniqueness_of_kernel, the public statement of the T5 theorem that takes primitive cost hypotheses and routes through the AczelRegularityKernel. It supports the forcing chain step T5 by ensuring that smooth solutions to the d'Alembert equation meet the differentiability class needed for the cosh identification without extra hypotheses.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.