slowRollEpsilon
The first slow-roll parameter ε is defined as half the square of the logarithmic derivative of the J-cost potential V(φ). Early-universe cosmologists cite this expression when extracting the scalar spectral index and tensor-to-scalar ratio from recognition-based inflation models. The definition evaluates the explicit derivative of J and applies the standard formula with a guard that returns zero if the potential vanishes.
claim$ε(φ) = ½ (V'(φ)/V(φ))² for φ > 0, where V(φ) is the J-cost function and V'(φ) = (1 - φ^{-2})/2.
background
The module COS-001 treats cosmic inflation as slow roll of the J-cost field. The inflaton potential is identified with the J-cost J(φ) = ½(φ + φ^{-1}) - 1, which is parabolic near its minimum at φ = 1 and linear at large φ. Upstream, the inflatonPotential definition returns exactly this J-cost, while the structural slow-roll parameter supplies the closed form 1/(2φ^5).
proof idea
The definition binds V to the inflatonPotential result and Vp to the closed-form derivative (1 - 1/φ²)/2, then returns (Vp/V)²/2 when V > 0 and zero otherwise.
why it matters in Recognition Science
This definition is invoked directly by the spectralIndex and tensorScalarRatio definitions to produce the observable predictions n_s ≈ 0.96 and r ≈ 8/N². It supplies the concrete link between the J-cost structure and the standard slow-roll observables required by the COS-001 mechanism. The parent results in InflatonPotentialStructural certify positivity of ε.
scope and limits
- Does not prove ε remains below 1 throughout the inflationary regime.
- Does not integrate the slow-roll trajectory equations.
- Does not address reheating or the exit from inflation.
- Does not evaluate numerical values for given initial φ.
formal statement (Lean)
68noncomputable def slowRollEpsilon (φ : ℝ) (hφ : φ > 0) : ℝ :=
proof body
Definition body.
69 -- V'(φ) = (1 - 1/φ²) / 2
70 -- V(φ) = (φ + 1/φ) / 2 - 1
71 let V := inflatonPotential φ hφ
72 let Vp := (1 - 1/φ^2) / 2
73 if V > 0 then (Vp / V)^2 / 2 else 0
74
75/-- Second slow-roll parameter η = V''/V.
76 Inflation requires |η| < 1. -/