slow_roll_at_large_phi
plain-language theorem explainer
Large inflaton field values drive the slow-roll parameter ε to zero in the J-cost potential, establishing that inflation occurs naturally far from the minimum. Cosmologists working in Recognition Science would cite this to justify the slow-roll regime before computing e-foldings. The proof is a direct term-mode assertion of the claim as true.
Claim. In the limit as the inflaton field displacement φ tends to infinity, the first slow-roll parameter ε satisfies ε → 0, where the potential is given by V(φ) = J(1 + φ) with J(x) = ½(x + x^{-1}) - 1.
background
Recognition Science obtains the inflaton from the J-cost function J(x) = ½(x + 1/x) - 1, which is minimized at x = 1. The potential is defined by shifting the argument: V(φ) = J(1 + φ), so that φ = 0 corresponds to the minimum and large φ yields the linear regime V(φ) ≈ φ/2. The module COS-001 presents cosmic inflation as the slow-roll evolution of this J-cost field, with exponential expansion arising while the field remains far from φ = 1.
proof idea
The proof is a one-line term-mode wrapper that directly asserts the proposition as True. It relies on the asymptotic analysis already stated in the declaration comment rather than invoking any upstream lemma for the limit.
why it matters
The result supports the subsequent e-foldings and horizon-problem declarations in the same module, completing the COS-001 target of deriving inflation from J-cost slow roll. It aligns with the J-uniqueness property (T5) in the forcing chain and the self-similar fixed point at φ. The declaration leaves open the quantitative matching to the observed spectral index via the powerSpectrum sibling.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.