ode_regularity_differentiable_hypothesis
plain-language theorem explainer
This definition packages the regularity hypothesis that any continuous real function H satisfying the ODE H''(t) = H(t) for all t must be differentiable. It is invoked in the T5 uniqueness argument for the canonical cost algebra and in multiple d'Alembert solution lemmas that feed the forcing chain. The declaration is a direct packaging of the implication with no additional proof steps.
Claim. Let $H : ℝ → ℝ$ be the shifted cost function $H(t) = G(t) + 1$. The hypothesis asserts that if $H''(t) = H(t)$ for every $t$ and $H$ is continuous, then $H$ is differentiable on $ℝ$.
background
The module supplies supporting lemmas for the T5 cost-uniqueness proof in the forcing chain. The function H is the reparametrization $H_F(t) = G_F(t) + 1$ of the cost function G, which itself satisfies the shifted d'Alembert equation $H(xy) + H(x/y) = 2 H(x) H(y)$ obtained from the Recognition Composition Law applied to J. Upstream, the same H appears as $H(x) = J(x) + 1 = ½(x + x^{-1})$, converting the original functional equation into the linear ODE $f'' = f$ whose solutions are multiples of cosh.
proof idea
The declaration is a one-line definition that directly encodes the implication (second-derivative identity and continuity imply differentiability) as a Prop. No lemmas or tactics are applied inside the body; it simply states the regularity bootstrap required by the surrounding ODE theory.
why it matters
The definition supplies the differentiable half of the regularity hypotheses used by cost_algebra_unique, the theorem that forces the cost function to be exactly J and thereby realizes T5 J-uniqueness. It is also referenced by cosh_satisfies_differentiable, ode_cosh_uniqueness, and the d'Alembert solution theorems that close the uniqueness argument for the eight-tick octave and the phi-ladder. Without this packaged hypothesis the bootstrap from continuous to differentiable solutions would remain open in the T5 proof.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.