Gspher_negative_at_pi
plain-language theorem explainer
The spherical cost function Gspher(t) = cos(t) - 1 evaluates negatively at t = π. Researchers working on the curvature gate cite this result to exclude spherical geometry from admissible cost metrics. The proof is a direct term-mode simplification that unfolds the definition, substitutes the value of cosine at π, and normalizes the resulting number.
Claim. Let $G(t) = 1 - F(e^t)$ be the log-coordinate cost. For the spherical candidate $G(t) := 1 - F(e^t)$ with $F$ satisfying the spherical ODE, one has $G(π) < 0$.
background
The Curvature Gate module requires constant nonzero curvature for the metric ds² = G''(t) dt² induced by the log-reparametrization G(t) = F(exp t). Three constant-curvature solutions are distinguished: flat (G(t) = t²/2), hyperbolic (G(t) = cosh(t) - 1, from the Recognition Composition Law), and spherical (Gspher(t) = cos(t) - 1). The spherical case is introduced precisely to exhibit eventual negativity, as stated in the module: spherical geometry produces periodic comparisons that violate F ≥ 0.
proof idea
The proof is a one-line term wrapper. It applies simp to replace Gspher by its definition cos t - 1 and to insert cos π = -1, then invokes norm_num to discharge the concrete numerical inequality -2 < 0.
why it matters
This theorem is the key step feeding Gspher_violates_nonnegativity, which concludes that the spherical solution fails IsNonNegativeG. It thereby closes the curvature-gate argument that only the hyperbolic solution (tied to T5 J-uniqueness and the Recognition Composition Law) survives the non-negativity requirement, consistent with D = 3 and the eight-tick octave in the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.