ode_regularity_bootstrap_of_smooth
plain-language theorem explainer
Any infinitely differentiable real-valued function H satisfies the linear ODE regularity bootstrap hypothesis. Researchers proving T5 J-uniqueness in Recognition Science cite this to close the smoothness step in the Aczél formulation of the d'Alembert equation. The proof is a one-line wrapper that invokes the ContDiff ordering lemma.
Claim. If $H : ℝ → ℝ$ is infinitely differentiable, then the following implication holds: whenever $H''(t) = H(t)$ for all $t$, $H$ is continuous, and $H$ is differentiable, it follows that $H$ is twice continuously differentiable.
background
The module Cost.FunctionalEquation supplies lemmas for the T5 cost uniqueness proof. Here H is the shifted cost reparametrization H(t) = G(t) + 1, where G satisfies the d'Alembert identity H(xy) + H(x/y) = 2 H(x) H(y) under the Recognition Composition Law. The referenced hypothesis ode_linear_regularity_bootstrap_hypothesis asserts that pointwise satisfaction of the linear ODE f'' = f, together with continuity and differentiability, implies C² regularity. Upstream, dAlembert_cosh_solution shows that continuous solutions with H(0) = 1 and H''(0) = 1 equal cosh, while CostAlgebra.H records the shift from J-cost to this H form.
proof idea
This is a one-line wrapper that applies the ContDiff ordering lemma (h.of_le le_top) to deduce that ContDiff ℝ ⊤ immediately yields the C² conclusion required by the bootstrap hypothesis.
why it matters
The declaration closes the regularity gap inside the T5 J-uniqueness argument. It is invoked by primitive_to_uniqueness_of_kernel in AczelClassification, the public statement of T5 that routes through the Aczél kernel, and by the corresponding theorem in FunctionalEquationAczel. In the framework it supports the passage from d'Alembert solutions to the cosh form under T5, consistent with the eight-tick octave and phi-ladder structure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.