ode_regularity_continuous_of_smooth
plain-language theorem explainer
If a real function H is infinitely differentiable then it satisfies the ODE regularity hypothesis that any solution to f''=f is continuous. Uniqueness proofs for the cost functional equation under Aczél assumptions cite this lemma to convert smoothness into the required continuity. The proof is a one-line wrapper that extracts continuity directly from the ContDiff assumption.
Claim. Let $H:ℝ→ℝ$. If $H$ is infinitely differentiable, then whenever $H''(t)=H(t)$ for all $t$, it follows that $H$ is continuous.
background
The module isolates legacy Aczél-dependent closure theorems for the functional equation uniqueness. The shifted cost is defined by $H(x)=J(x)+1=½(x+x^{-1})$, turning the Recognition Composition Law into the d'Alembert equation $H(xy)+H(x/y)=2H(x)H(y)$. Upstream results introduce two ODE regularity hypotheses: ode_regularity_continuous_hypothesis states that $f''=f$ implies continuity, while ode_regularity_differentiable_hypothesis adds differentiability once continuity is known.
proof idea
This is a one-line wrapper that applies the fact that ContDiff ℝ ⊤ H directly yields Continuous H, without using the ODE assumption.
why it matters
The declaration supplies the third ODE regularity step that feeds primitive_to_uniqueness_of_kernel in AczelClassification, the public T5 theorem with explicit Aczél kernel seam. It closes the smoothness-to-continuity bridge needed for J-uniqueness (T5) in the forcing chain while the core FunctionalEquation module remains axiom-free.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.