slowRollEpsilon
plain-language theorem explainer
This definition sets the slow-roll parameter ε to 1/(2φ^5) for the Recognition Science inflaton potential. Cosmologists working in the J-cost framework cite it when deriving the spectral index and tensor-to-scalar ratio. It is a direct constant assignment obtained by substituting the specific potential into the general slow-roll expression.
Claim. The first slow-roll parameter satisfies $ε = 1/(2 φ^5)$.
background
The module establishes the inflaton potential with five structural regimes for configDim D = 5. It lists the slow-roll parameters explicitly as ε = 1/(2φ^5), η = 1/φ^5, together with n_s - 1 = -2/45 and r = 2/(45 φ²), and states that the e-fold count equals 44. The upstream result from the Inflation module defines the general slow-roll parameter as ε = (V'/V)^2 / 2 and requires ε < 1 for inflation to occur.
proof idea
One-line definition that directly assigns the constant 1/(2 φ^5).
why it matters
This supplies the concrete ε used by the spectral index and tensor-to-scalar ratio definitions. It enters the InflatonCert structure that certifies the five regimes, 44 e-folds, and positivity conditions. The φ^5 scaling realizes the phi-ladder from the forcing chain T5-T8 and matches the RS-native constants ħ = φ^{-5} and G = φ^5 / π.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.