ode_linear_regularity_bootstrap_hypothesis_neg
plain-language theorem explainer
The definition encodes the regularity bootstrap hypothesis for solutions to the linear ODE H'' = -H. Researchers proving uniqueness for the cosine branch of the d'Alembert equation in Recognition Science cite it when closing smoothness from pointwise derivative conditions. It packages the implication that pointwise second-derivative equality plus continuity and differentiability yields C² regularity, serving as a standard hypothesis in the angle coupling proofs.
Claim. Let $H : ℝ → ℝ$. The property that if $H''(t) = -H(t)$ holds for all $t$, and $H$ is continuous and differentiable, then $H$ is twice continuously differentiable.
background
The module develops the cosine branch of the d'Alembert functional equation $H(t+u) + H(t-u) = 2 H(t) H(u)$ with calibration $H''(0) = -1$, which selects the cosine solution under Aθ1–Aθ4. Upstream definitions from CostAlgebra and FunctionalEquation introduce the shifted cost $H(x) = J(x) + 1$ satisfying the positive d'Alembert identity, supplying the parallel structure for the negative-curvature angle case. This hypothesis forms one component of the AngleStandardRegularity structure that packages the Aczél regularity assumptions.
proof idea
The declaration is a direct definition of the Prop that states the bootstrap implication for the negative linear ODE. It is applied verbatim as a hypothesis in downstream results such as cos_satisfies_bootstrap_neg and ode_cos_uniqueness.
why it matters
It supplies the regularity link required for the angle T5 theorem, feeding directly into dAlembert_cos_solution and ode_cos_uniqueness to conclude $H = cos$ from the functional equation plus $H''(0) = -1$. This closes the smoothness scaffolding for the cosine branch, mirroring the cosh branch in Cost.FunctionalEquation and supporting the forcing chain distinction between positive and negative curvature.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.