slow_roll_eta
plain-language theorem explainer
The slow-roll parameter η is defined for the J-cost inflaton potential G(t) = cosh(t) - 1 as the ratio of its second derivative to the normalized height G(t) + 1. This yields the constant value 1 for all real t, placing the potential at the exact self-similar fixed point required by the Recognition Composition Law. Cosmologists studying alpha-attractor models would cite this to derive the spectral index from J-cost curvature. The definition is realized as the direct ratio cosh(t)/cosh(t) using the hyperbolic form of G.
Claim. $η(t) := G''(t) / (G(t) + 1)$ where $G(t) = cosh(t) - 1$ is the J-cost in logarithmic coordinates $t = ln(x)$. This expression equals 1 for all real $t$.
background
The JCostInflaton module identifies the inflaton potential with the J-cost under a logarithmic change of variables. G is defined by G(t) := cosh(t) - 1, which follows directly from J(x) = (x + x^{-1})/2 - 1 satisfying the Recognition Composition Law. The slow-roll parameters are extracted from the derivatives of this G, with η measuring curvature relative to the normalized potential height.
proof idea
This is a direct definition that sets slow_roll_eta t to Real.cosh t / Real.cosh t. It follows immediately from substituting the second derivative of G (cosh t) and the normalized potential (G + 1 = cosh t) into the standard expression for η. No additional lemmas are required beyond the definition of G.
why it matters
The definition supplies the input to the sibling theorem eta_eq_one, which proves η equals 1 identically. This confirms that the J-cost potential is perfectly self-similar, consistent with T5 J-uniqueness and the derivation of alpha-attractor inflation from the Recognition Composition Law. It contributes to the chain leading to the spectral index 1 - 2/N and the master certificate InflationFromJCostCert.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.