epsilon_nonneg
plain-language theorem explainer
The slow-roll parameter ε derived from the J-cost potential in logarithmic coordinates is non-negative for every real t. Inflation modelers using α-attractor potentials would cite the result to verify that the derived ε satisfies the basic slow-roll inequality before computing spectral indices. The proof is a one-line wrapper that unfolds the definition of ε and invokes the positivity tactic on the resulting expression.
Claim. For every real number $t$, the slow-roll parameter $ε(t)$ constructed from the potential $G(t)=cosh(t)-1$ satisfies $ε(t)≥0$.
background
In the J-Cost as the Inflaton Potential module the Recognition Composition Law is re-expressed in logarithmic coordinates via the auxiliary function $G(t)=J(e^t)$, which evaluates to $cosh(t)-1$. This yields the plateau potential whose vacuum lies at $t=0$, with $G(0)=0$, $G'(0)=0$ and $G''(0)=1$. The slow-roll parameter is then defined from the normalized curvature of $G$ exactly as in the standard α-attractor literature: $ε=(G')^2/(2(G+1)^2)$. Upstream results supply the underlying cost function (MultiplicativeRecognizerL4.cost) and the gravitational constant reparametrization (Constants.G and Cost.FunctionalEquation.G) that together guarantee the expression for $G$ is well-defined on the positive reals.
proof idea
The proof is a one-line wrapper. It unfolds the definition of slow_roll_epsilon to expose the explicit algebraic form built from derivatives of $G$, then applies the positivity tactic, which recognizes the expression as a square divided by a positive denominator.
why it matters
Non-negativity of ε is the first concrete check that the J-cost potential satisfies the slow-roll regime required for the α-attractor identification and the subsequent derivation of the spectral index $1-2/N$. It sits inside the chain that begins with T5 (J-uniqueness) and T6 (phi fixed point) and feeds the master certificate InflationFromJCostCert listed in the module documentation. Because the used-by count is currently zero, the lemma remains a local prerequisite rather than a cited parent theorem.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.