slowRollEpsilon_pos
plain-language theorem explainer
The theorem establishes that the slow-roll parameter ε exceeds zero under the Recognition Science inflaton definition. Cosmologists verifying early-universe slow-roll conditions would cite it when assembling the inflaton certificate. The proof unfolds the explicit form ε = 1/(2 φ^5) and chains the standard positivity lemmas div_pos and mul_pos.
Claim. $0 < 1/(2 φ^5)$ where $φ > 0$ denotes the inflaton field value in the RS model.
background
The InflatonPotentialStructural module specializes the slow-roll parameter ε to the closed form 1/(2 φ^5). This follows the general definition ε = (V'/V)^2 / 2 supplied by the upstream Inflation module, where the potential is V(φ) = (φ + 1/φ)/2 - 1. The module states five canonical regimes for the RS inflaton potential with D = 5 and records the explicit slow-roll parameters ε = 1/(2φ^5), η = 1/φ^5.
proof idea
The term-mode proof first unfolds slowRollEpsilon to the division 1 / (2 * phi ^ 5). It applies div_pos to the positive numerator 1 and the positive denominator, the latter obtained by mul_pos of a norm_num constant and pow_pos applied to phi_pos raised to the fifth power.
why it matters
The result supplies the epsilon_pos field required by the downstream inflatonCert certificate that aggregates the five regimes, e-fold count, and positivity of both slow-roll parameters. It closes the verification step for the slow-roll plateau regime inside the A2-depth analysis of the inflaton potential, consistent with the phi-ladder and eight-tick octave structure of the framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.