slow_roll_epsilon
plain-language theorem explainer
The slow-roll parameter ε is defined by ε(t) = sinh²(t) / (2 cosh²(t)) for the potential G(t) = cosh(t) - 1. Cosmologists deriving α-attractor predictions from the Recognition Composition Law would cite this when converting the J-cost into slow-roll parameters. The definition follows by substituting the derivatives of G into the normalized slow-roll formula ε = (V')² / (2(V+1)²).
Claim. $ε(t) = sinh²(t) / (2 cosh²(t))$, the first slow-roll parameter for the potential $G(t) = cosh(t) - 1$ obtained from the J-cost in logarithmic coordinates.
background
The module treats the J-cost as an inflaton potential. In log coordinates t = ln(x) the J-cost takes the explicit form G(t) = cosh(t) - 1, which is the exact image of J(x) = ½(x + x⁻¹) - 1 under the substitution x = eᵗ. This yields the plateau potential with G(0) = 0, G'(0) = 0 and G''(0) = 1, matching the calibration constant A3 of the forcing chain.
proof idea
One-line definition that sets slow_roll_epsilon t directly to sinh²(t) / (2 cosh²(t)), reproducing the standard slow-roll expression once V = G and V + 1 = cosh(t) are substituted.
why it matters
This supplies the explicit ε used by epsilon_formula, epsilon_le_half, epsilon_nonneg and the master certificate InflationFromJCostCert. It completes the step from J-uniqueness (T5) and the Recognition Composition Law to the slow-roll parameters that produce n_s = 1 - 2/N and r = 12 φ² / N². The definition therefore anchors the α-attractor identification α = φ² inside the eight-tick octave framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.