potential_min_at_one
plain-language theorem explainer
The J-cost potential for the inflaton field attains its global minimum at field value 1. Cosmologists working in the Recognition Science framework cite this to mark the termination of slow-roll inflation. The term-mode proof unfolds the potential definition, substitutes the unit value Jcost 1 = 0, and invokes non-negativity of Jcost for positive arguments.
Claim. Let $V(φ) = J(φ)$ be the inflaton potential for $φ > 0$, where $J$ denotes the J-cost function. Then $V(φ) ≥ V(1)$.
background
In the COS-001 module the inflaton is identified with the J-cost scalar field whose potential is exactly the function $J(φ) = ½(φ + 1/φ) - 1$. This function is nonnegative for $φ > 0$ by the AM-GM inequality and equals zero only at $φ = 1$. The module documentation states that inflation arises from slow roll of this field, with the minimum at $φ = 1$ ending the exponential-expansion phase.
proof idea
The proof unfolds the definition of inflatonPotential to Jcost φ. It then applies the lemma Jcost_unit0 to replace the right-hand side by zero and concludes with the lemma Jcost_nonneg that Jcost φ is nonnegative whenever φ > 0.
why it matters
The result supplies the lower bound required for all subsequent slow-roll analysis in the same module. It confirms the parabolic shape near the minimum described in the module documentation and anchors the termination of inflation before the derivations of e-foldings and the horizon, flatness, and monopole problems. The theorem therefore closes the basic potential properties in the J-cost treatment of cosmic inflation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.