ode_regularity_continuous_hypothesis
plain-language theorem explainer
The declaration encodes the regularity claim that any function H satisfying the pointwise ODE H''(t) = H(t) for all t must be continuous. It is cited in the T5 uniqueness proof for the canonical cost function J and in the derivation of cosh as the unique solution to the d'Alembert equation. The definition is a direct implication with no additional lemmas or tactics.
Claim. Let $H : ℝ → ℝ$ be the shifted cost function. If $H''(t) = H(t)$ holds for every real $t$, then $H$ is continuous.
background
The module supplies functional-equation helpers for the T5 cost-uniqueness argument in the forcing chain. H is the shifted cost reparametrization H(t) = G(t) + 1, equivalently H(x) = J(x) + 1 where J satisfies the Recognition Composition Law. Under this shift the RCL reduces to the d'Alembert equation H(xy) + H(x/y) = 2 H(x) H(y), as stated in the upstream CostAlgebra.H definition.
proof idea
The declaration is a direct definition of the proposition as the implication (∀ t, deriv (deriv H) t = H t) → Continuous H. No lemmas are invoked; it simply names the regularity statement for use as a hypothesis.
why it matters
It is required by the main theorem cost_algebra_unique, which states that any CostAlgebraData obeying the axioms plus the calibration J''(1) = 1 must recover the canonical J. This completes the T5 J-uniqueness step. The same hypothesis appears in ode_cosh_uniqueness, dAlembert_to_ODE_theorem, and the cosh-solution theorems, all of which rely on the eight-tick octave and D = 3 structure downstream.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.