V_nonneg
plain-language theorem explainer
The theorem shows the inflaton potential V(φ_inf) stays nonnegative for all real φ_inf > -1. Cosmologists building recognition-based inflation models cite it to confirm a lower bound at the vacuum. The proof is a one-line wrapper that unfolds V to Jcost(1 + φ_inf), applies the Jcost nonnegativity lemma, and uses linarith to check the argument is positive.
Claim. For every real number $φ_{inf} > -1$, the inflaton potential satisfies $V(φ_{inf}) ≥ 0$, where $V(φ_{inf}) := J(1 + φ_{inf})$ and $J$ is the recognition cost function.
background
The module defines the inflaton potential on the recognition manifold by V(φ_inf) := Jcost(1 + φ_inf), where φ_inf measures dimensionless displacement from the canonical reference rung. Jcost is the recognition cost function drawn from the Cost module. Its upstream lemma Jcost_nonneg states that J(x) ≥ 0 for positive x by the AM-GM inequality, quoted directly as 'J(x) ≥ 0 for positive x (AM-GM inequality)'.
proof idea
The proof is a term-mode wrapper. It unfolds the definition of V to expose Jcost(1 + phi_inf), applies the lemma Jcost_nonneg from Cost, and invokes linarith to confirm that -1 < phi_inf forces 1 + phi_inf > 0.
why it matters
This supplies the nonnegativity field inside inflatonPotentialCert, the certificate that collects vacuum value, positivity off vacuum, reciprocal symmetry, and quadratic form for the potential. It completes the module's task of writing an explicit inflaton field on the recognition manifold, grounding slow-roll parameters in the Taylor coefficients of J. The result ties directly to the J-cost that appears throughout the framework's forcing chain and phi-ladder constructions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.