ode_regularity_differentiable_of_smooth
plain-language theorem explainer
Any infinitely differentiable real-valued function H satisfies the regularity hypothesis that pointwise equality of its second derivative to itself, together with continuity, implies differentiability. Researchers tracing the Aczel route to T5 cost uniqueness cite this lemma. The proof is a one-line term that extracts C^1 regularity from C^∞ via the ContDiff hierarchy and invokes the standard differentiability predicate.
Claim. Let $H:ℝ→ℝ$ be infinitely differentiable. Then the following holds: if $H''(t)=H(t)$ for all $t∈ℝ$ and $H$ is continuous, then $H$ is differentiable.
background
The module supplies helper lemmas for the T5 cost uniqueness proof. Here H denotes a general real function (reparametrizing the shifted cost G+1) that is assumed to obey the linear ODE f''=f. The hypothesis in question is the statement that pointwise satisfaction of the ODE plus continuity forces differentiability. Upstream, the shifted cost H(x)=J(x)+1=½(x+x^{-1}) converts the Recognition Composition Law into the d'Alembert equation H(xy)+H(x/y)=2H(x)H(y).
proof idea
The proof is a one-line term wrapper. It applies the ContDiff hierarchy to obtain C^1 regularity from C^∞ (via of_le le_top), then invokes the Mathlib fact that every C^1 function is differentiable.
why it matters
This lemma closes a regularity step in the chain leading to the public T5 theorem primitive_to_uniqueness_of_kernel. That theorem uses an explicit AczelRegularityKernel seam to conclude that the only solutions are the J-cost functions, directly supporting T5 J-uniqueness in the forcing chain. It supplies the differentiability half of the ODE bootstrap without external analysis.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.