ode_regularity_continuous_hypothesis_neg
The declaration defines the proposition that any real function H obeying the ODE H''(t) = -H(t) for all t is necessarily continuous. It is cited inside the regularity bundle that supports uniqueness for the cosine solution of the d'Alembert equation on the angle-coupling branch. The body is a direct implication with no further reduction steps.
claimLet $H : ℝ → ℝ$. Then $(∀ t ∈ ℝ, H''(t) = -H(t)) ⇒ H$ is continuous.
background
The module treats the d'Alembert functional equation H(t+u) + H(t-u) = 2 H(t) H(u) under the negative-calibration condition H''(0) = -1, which isolates the cosine branch parallel to the cosh branch on the cost side. Upstream, H is introduced as the shifted reparametrization H = J + 1, converting the Recognition Composition Law into standard d'Alembert form. The present definition isolates the continuity consequence of the ODE H'' = -H, which is required before smoothness and uniqueness results can be applied.
proof idea
The declaration is a direct definition of the implication from the twice-differentiable ODE condition to continuity of H. It functions as a named hypothesis interface with no internal lemmas or tactics.
why it matters in Recognition Science
It supplies the continuity clause inside the AngleStandardRegularity structure, which packages Aθ2 and feeds dAlembert_cos_solution (the Angle T5 theorem) and ode_cos_uniqueness. The definition mirrors the corresponding cost-side regularity statements and closes the regularity step in the T5 forcing chain for the cosine branch. It touches the bootstrap question of obtaining full smoothness from the ODE alone.
scope and limits
- Does not assert existence of any solution to the ODE.
- Does not derive the ODE from the d'Alembert equation.
- Does not impose normalization conditions such as H(0) = 1.
- Does not establish differentiability, only continuity from the ODE assumption.
formal statement (Lean)
195def ode_regularity_continuous_hypothesis_neg (H : ℝ → ℝ) : Prop :=
proof body
Definition body.
196 (∀ t, deriv (deriv H) t = -H t) → Continuous H
197
198/-- **ODE regularity: differentiable solutions.** -/