SatisfiesSphericalODE
plain-language theorem explainer
SatisfiesSphericalODE encodes the predicate that a cost function G in log coordinates obeys the second-order ODE G''(t) = -(G(t) + 1). Researchers classifying constant-curvature solutions in the curvature gate cite this predicate when partitioning candidates into flat, hyperbolic, or spherical cases. The definition is a direct universal quantification on the second derivative with no auxiliary lemmas.
Claim. A function $G : ℝ → ℝ$ satisfies the spherical ODE when its second derivative obeys $G''(t) = -(G(t) + 1)$ for every real $t$.
background
The CurvatureGate module formalizes the requirement that the cost metric has constant nonzero curvature. In log coordinates the reparametrization G(t) := F(e^t) produces the 1D metric ds² = G''(t) dt², with three constant-curvature cases distinguished by the sign of κ: flat (G(t) = t²/2), hyperbolic (G(t) = cosh(t) - 1), and spherical (G(t) = cos(t) - 1). The upstream definition of G appears in Cost.FunctionalEquation as the composition F ∘ exp, while the module documentation states that spherical solutions are ruled out by non-negativity of F.
proof idea
The definition is introduced directly as the universal statement ∀ t, deriv (deriv G) t = -(G t + 1). No lemmas are invoked; it functions as the target predicate for verification theorems such as Gspher_satisfies_spherical.
why it matters
This predicate supplies the spherical branch of the trichotomy used by curvature_gate_dichotomy, curvature_gate_main, and curvature_gate_summary. Those theorems apply calibration (G''(0) = 1) and non-negativity to eliminate the spherical case, leaving only flat or hyperbolic solutions and thereby forcing the Recognition Composition Law. It closes the spherical option in the curvature gate, consistent with the framework requirement that recognition geometry be non-trivially curved.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.