epsilon_le_half
plain-language theorem explainer
The slow-roll parameter ε(t) = sinh²(t)/(2 cosh²(t)) from the J-cost inflaton potential in log coordinates satisfies ε(t) ≤ 1/2 for every real t. Model builders deriving α-attractor predictions from Recognition Science would cite this to keep the plateau potential inside the slow-roll window. The proof is a direct algebraic reduction that applies the hyperbolic identity cosh² - sinh² = 1 together with nlinarith bounds on the squared terms.
Claim. For all real $t$, let $V(t) = G(t) = cosh(t) - 1$. Then the slow-roll parameter defined by $ε(t) = sinh²(t) / (2 cosh²(t))$ obeys $ε(t) ≤ 1/2$.
background
The JCostInflaton module identifies the inflaton potential with the J-cost in logarithmic coordinates: G(t) = cosh(t) - 1 where t = ln(x) and J(x) = (x + x^{-1})/2 - 1. This follows from the Recognition Composition Law and J-uniqueness. The first slow-roll parameter is defined explicitly as ε(t) = sinh²(t) / (2 cosh²(t)), which is the standard form (V')² / (2(V+1)²) once V is taken as G and normalized by the +1 shift that converts cosh(t) into the denominator.
proof idea
The proof unfolds the definition of slow_roll_epsilon, invokes Real.cosh_pos and the identity Real.cosh_sq_sub_sinh_sq, then uses positivity and nlinarith to obtain sinh²(t) ≤ (1/2)·(2 cosh²(t)). The final calc step divides both sides by the positive quantity 2 cosh²(t) and simplifies the right-hand side to 1/2.
why it matters
This bound is invoked directly as epsilon_bounded inside the master certificate inflation_from_jcost_cert, which states that every ingredient of the inflationary prediction chain is forced by J-cost uniqueness. It supports the α-attractor identification α = φ² that follows from G''(0) = 1 and the phi fixed point, and it closes the slow-roll analysis required for the eight-tick octave and D = 3 spatial setting.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.