ode_linear_regularity_bootstrap_hypothesis
plain-language theorem explainer
The declaration packages the regularity bootstrap for the linear ODE H'' = H: any function satisfying the second-derivative equation pointwise, together with continuity and differentiability, is automatically C². Researchers establishing uniqueness of the J-cost in the T5 forcing chain cite it when discharging smoothness assumptions inside d'Alembert-type arguments. The definition is a direct encoding of the standard ODE regularity implication drawn from Mathlib.
Claim. Let $H : ℝ → ℝ$. The hypothesis asserts that if $H''(t) = H(t)$ holds for all $t$, $H$ is continuous, and $H$ is differentiable, then $H$ is twice continuously differentiable.
background
The module supplies functional-equation helpers for the T5 step of the forcing chain, which establishes J-uniqueness. Here H is the shifted cost function H(t) = G(t) + 1, where G reparametrizes the J-cost; the upstream CostAlgebra.H redefines the same object as H(x) = J(x) + 1 = ½(x + x⁻¹), converting the Recognition Composition Law into the d'Alembert equation H(xy) + H(x/y) = 2 H(x) H(y). The local setting therefore treats the linear ODE H'' = H as the analytic counterpart of that functional equation.
proof idea
The definition directly encodes the implication from pointwise second-derivative equality plus continuity and differentiability to ContDiff ℝ 2 H. It is a one-line wrapper that packages the standard result on linear ODEs with constant coefficients, to be discharged later by Mathlib's ContDiff lemmas (as seen in the sibling cosh_satisfies_bootstrap).
why it matters
The hypothesis is invoked inside cost_algebra_unique to conclude that any CostAlgebraData obeying the axioms and calibration J''(1) = 1 must recover the canonical J-cost; it likewise feeds ode_cosh_uniqueness and the dAlembert_cosh_solution family. In the Recognition framework it closes the regularity gap between the algebraic T5 uniqueness statement and the analytic identification of solutions with cosh, without requiring a full Picard-Lindelöf development.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.