epsilon_formula
plain-language theorem explainer
The theorem states that the slow-roll parameter ε(t) for the J-cost inflaton potential equals sinh²(t) over 2 cosh²(t). Cosmologists working with α-attractors derived from the Recognition Composition Law would cite this explicit form. The proof holds by reflexivity after the definition of slow_roll_epsilon unfolds from the derivatives of G(t) = cosh(t) − 1.
Claim. For the first slow-roll parameter ε(t) of the potential G(t) = cosh(t) − 1 in logarithmic coordinates, ε(t) = sinh²(t) / (2 cosh²(t)).
background
The JCostInflaton module identifies the inflaton potential with the J-cost reparametrized as G(t) := J(exp t) = cosh(t) − 1. This form arises because the Recognition Composition Law forces J(x) = (x + x⁻¹)/2 − 1, which becomes the Starobinsky plateau in log time t. The slow-roll parameters follow the standard definitions ε = (G')² / (2(G + 1)²) and η = G'' / (G + 1) after normalization by the module's V + 1 convention. Upstream, Constants.G supplies the RS-native gravitational constant while Cosmology.InflatonPotentialFromJCost.V sets V(φ_inf) = J(1 + φ_inf), and Cost.FunctionalEquation.G performs the log reparametrization.
proof idea
The proof is a one-line term proof by reflexivity (rfl). It succeeds because the right-hand side is exactly the algebraic simplification of slow_roll_epsilon(t) once the derivatives of G(t) = cosh(t) − 1 are substituted into the definition of ε.
why it matters
This supplies the explicit closed-form expression for ε in the J-cost inflation model. It feeds the module's derivations of the spectral index 1 − 2/N and the α = φ² identification from G''(0) = 1. The result sits inside the forcing chain after T6 (phi as self-similar fixed point) and T7 (eight-tick octave), confirming that the Recognition Composition Law produces the canonical slow-roll trajectory without additional assumptions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.