slowRollEta
plain-language theorem explainer
The slow-roll parameter η is fixed at the constant value 1/φ^5 in RS-native units. Cosmologists modeling inflation would cite this when computing the scalar spectral index or populating the InflatonCert structure that verifies the five-regime potential. The definition is a direct assignment that specializes the general V''/V expression at the self-similar fixed point.
Claim. The second slow-roll parameter is given by $η = φ^{-5}$, where $φ$ denotes the self-similar fixed point satisfying $φ^5 = 5φ + 3$.
background
The Inflaton Potential Structural module fixes the RS inflaton potential across five regimes (slow-roll plateau, slope, hilltop decline, reheating, post-reheating radiation) that match configDim D = 5. Slow-roll parameters are set at ε = 1/(2φ^5) and η = 1/φ^5, which immediately yield n_s - 1 = -2/45 and r = 2/(45 φ²) together with an e-fold count of 44. This constant η specializes the general definition η(φ) = V''(φ)/V(φ) from the parent Inflation module, where V''(φ) = 1/φ^3 for the inflaton potential V.
proof idea
The declaration is a one-line definition that directly assigns the value 1/φ^5. It relies on the imported phi constant from Constants together with the Fibonacci identity φ^5 = 5φ + 3 noted in the module comment.
why it matters
This definition supplies the numerical η required by the InflatonCert structure that certifies the five-regime potential and by the spectralIndex computation that produces n_s ≈ 0.96. It anchors the A2 cosmology section to the phi-ladder fixed point (T6) and the eight-tick octave (T7) from the forcing chain. The downstream slowRollEta_pos theorem then establishes positivity from this value, confirming n_s lies in (0.955, 0.957).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.