G_nonneg
plain-language theorem explainer
G_nonneg establishes that the inflaton potential G(t) = cosh(t) - 1 is nonnegative for every real t. Model builders working with Recognition-derived alpha-attractors cite it to confirm the vacuum is a global minimum. The proof is a one-line wrapper that unfolds the definition of G and applies the standard inequality cosh(t) ≥ 1 via linear arithmetic.
Claim. For every real number $t$, the function $G$ defined by $G(t) := 2^{-1}(e^{t} + e^{-t}) - 1$ satisfies $G(t) ≥ 0$.
background
The module derives the inflaton potential from the J-cost under the Recognition Composition Law. In log coordinates the potential is defined by G(t) := cosh(t) - 1, which is exactly J(e^t) with J(x) = ½(x + x^{-1}) - 1. This produces the canonical plateau with G(0) = 0, G'(0) = 0 and G''(0) = 1, matching the calibration constant A3. Upstream results supply the reparametrization G_F t = F(exp t) from Cost.FunctionalEquation and the RS-native gravitational constant from Constants.
proof idea
The proof is a one-line wrapper. It unfolds the definition of G to obtain cosh(t) - 1, then invokes linarith on the library fact Real.one_le_cosh t.
why it matters
The result secures non-negativity of the J-cost potential, guaranteeing a stable vacuum endpoint for inflation. It underpins the slow-roll derivations (epsilon and eta) listed among the module siblings and recovers the spectral-index predictions of alpha-attractors from the curvature at t = 0. The non-negativity is required by the T5 J-uniqueness step in the forcing chain and by the phi-ladder mass formula.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.