slowRollEta_pos
plain-language theorem explainer
The theorem establishes that the second slow-roll parameter η remains strictly positive for the RS inflaton potential. Cosmologists verifying slow-roll conditions in the plateau regime would cite this result when building the inflaton certificate. The proof is a term-mode reduction that unfolds η to 1/φ^5 and applies the positivity lemmas div_pos and pow_pos.
Claim. $0 < 1/φ^5$ where φ > 0 is the inflaton field value in RS-native units.
background
The InflatonPotentialStructural module defines the slow-roll parameters for the RS inflaton potential V(χ) that admits five structural regimes at configDim D = 5. The local definition sets η = 1/φ^5. This rests on the upstream slowRollEta definition from the Inflation module, which expresses η = V''/V with V''(φ) = 1/φ^3. Module documentation states: Slow-roll parameters: ε = 1/(2φ⁵), η = 1/φ⁵, n_s - 1 = -2/45, r = 2/(45 φ²).
proof idea
The term proof first unfolds the definition of slowRollEta to 1/φ^5. It then applies div_pos to one_pos and the result of pow_pos phi_pos 5, which supplies the required positivity of the denominator.
why it matters
This positivity result is referenced inside the inflatonCert definition to certify the complete set of inflaton properties, including regime count, efold number, and positivity of both slow-roll parameters. It supplies the sign check for η required by the slow-roll analysis in the five-regime structure, consistent with the condition |η| < 1.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.