IsNonNegativeG
plain-language theorem explainer
The predicate IsNonNegativeG requires that a cost function G in log-coordinates satisfies G(t) ≥ 0 for every real t. Researchers formalizing the curvature gate cite it to exclude spherical geometries while retaining the hyperbolic solution. The definition is a direct universal quantifier with no further computation.
Claim. A function $G:ℝ→ℝ$ is non-negative when $G(t)≥0$ holds for all real $t$.
background
The module introduces the log-coordinate reparametrization $G(t)=F(e^t)$ that converts the cost metric to $ds^2=G''(t)dt^2$. Curvature classification then follows: flat ($κ=0$) yields the counterexample $t^2/2$, hyperbolic ($κ=-1$) recovers $cosh(t)-1$ from the Recognition Composition Law, and spherical ($κ=+1$) produces $1-cos(t)$ which fails positivity. Upstream, the JCostInflaton result supplies the explicit form $G(t)=cosh(t)-1$ that satisfies the inequality, while the module doc states that spherical space violates non-negativity and hyperbolic space encodes entangled comparisons.
proof idea
The definition is a direct universal quantification over the reals with no lemmas or tactics applied.
why it matters
It supplies the non-negativity hypothesis for the curvature_gate_main theorem, which concludes that non-negativity plus interaction forces the hyperbolic solution matching the RCL. The same predicate is used to prove that the spherical candidate Gspher violates the condition. In the framework it enforces the requirement that recognition geometry be non-trivially curved, ruling out flat independence and spherical periodicity.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.