ode_regularity_continuous_of_smooth
plain-language theorem explainer
Any infinitely differentiable function H from reals to reals satisfies the continuity hypothesis for solutions of the ODE f'' = f. Researchers proving T5 J-uniqueness via the Aczél kernel cite this to confirm that smooth cost candidates meet the required regularity. The proof is a one-line term that directly extracts continuity from the ContDiff assumption.
Claim. If $H : ℝ → ℝ$ is infinitely differentiable, then $(∀ t, H''(t) = H(t)) → H$ is continuous.
background
The Cost.FunctionalEquation module supplies helper lemmas for the T5 cost uniqueness proof. Here H is the shifted cost reparametrization H(t) = G(t) + 1, where the upstream CostAlgebra defines H(x) = J(x) + 1 = ½(x + x⁻¹) and converts the Recognition Composition Law into the d'Alembert equation H(xy) + H(x/y) = 2 H(x) H(y). The ode_regularity_continuous_hypothesis is the proposition (∀ t, deriv (deriv H) t = H t) → Continuous H, one of four regularity statements used to classify ODE solutions.
proof idea
The proof is a one-line term wrapper: it constructs the required implication by discarding the ODE premise and returning h.continuous directly from the ContDiff ℝ ⊤ hypothesis.
why it matters
This supplies ODE regularity (3) for the T5 J-uniqueness argument. It is invoked inside primitive_to_uniqueness_of_kernel to obtain continuity of H F once AczelRegularityKernel is assumed, and it appears in the AczelClassification path that makes the regularity seam explicit. The result aligns with the T5 step of the forcing chain, where J-uniqueness follows from the cosh fixed-point identity.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.