Gspher_violates_nonnegativity
plain-language theorem explainer
The spherical cost function G(t) = cos(t) - 1 violates the non-negativity condition required for valid recognition metrics in log-coordinates. Researchers formalizing the curvature gate cite this to exclude positive-curvature solutions from the allowed geometries. The proof assumes non-negativity, specializes the assumption to t = π, invokes the negativity lemma at that point, and derives a contradiction via linear arithmetic.
Claim. The function $G(t) := 1 - 1$ fails to satisfy $G(t) ≥ 0$ for all real $t$.
background
In the curvature gate module, cost metrics in log-coordinates are classified by curvature: flat (G(t) = t²/2), hyperbolic (G(t) = cosh(t) - 1), and spherical (G(t) = cos(t) - 1). The spherical solution satisfies the ODE G'' = G + 1 but is eventually negative. Non-negativity is defined as the property that G(t) ≥ 0 for every real t, ensuring the derived cost remains physically meaningful. The module states that spherical curvature produces periodic comparisons incompatible with this requirement, while hyperbolic curvature aligns with the Recognition Composition Law.
proof idea
The proof assumes non-negativity of Gspher, evaluates the assumption at t = π to obtain Gspher(π) ≥ 0, invokes the upstream lemma establishing Gspher(π) < 0, and applies linarith to reach a contradiction.
why it matters
This theorem rules out spherical curvature within the curvature gate, confirming that only the hyperbolic solution survives the non-negativity filter and thereby supports the requirement that recognition geometry must be non-trivially curved. It fills the explicit claim in the module that spherical space violates F ≥ 0. No downstream theorems depend on it directly, and it touches no open scaffolding.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.