Gspher_nonpositive
plain-language theorem explainer
The spherical curvature solution G(t) = cos(t) - 1 is non-positive for every real t. Researchers formalizing curvature constraints in one-dimensional metrics would cite this to exclude spherical geometry from the Recognition framework. The proof is a direct reduction to the elementary bound cos(t) ≤ 1 followed by linear arithmetic.
Claim. The spherical solution $G(t) := cos(t) - 1$ satisfies $G(t) ≤ 0$ for all real $t$.
background
The Curvature Gate module represents the cost metric in log-coordinates via G(t) = F(e^t), yielding the line element ds² = G''(t) dt². This produces three constant-curvature candidates: flat (G(t) = t²/2), hyperbolic (G(t) = cosh(t) - 1, linked to the Recognition Composition Law), and spherical (G(t) = cos(t) - 1). The spherical form is introduced explicitly as Gspher(t) := cos(t) - 1 to test against the non-negativity requirement on F. The module notes that spherical geometry produces periodic comparisons that violate this non-negativity.
proof idea
The proof introduces an arbitrary real t, simplifies the definition of Gspher to cos(t) - 1, invokes the standard inequality cos(t) ≤ 1, and closes with linear arithmetic.
why it matters
This result shows the spherical solution is non-positive, directly supporting the module's claim that spherical geometry is ruled out by F ≥ 0. It contributes to the Curvature Gate by eliminating the positive-curvature case and leaving hyperbolic geometry (tied to the Recognition Composition Law) as the remaining non-flat option. Within Recognition Science this aligns with the requirement of constant nonzero curvature and the exclusion of periodic structures.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.