spectralIndex

formal source

 134
 135/-- The scalar spectral index n_s.
 136    n_s = 1 - 6ε + 2η ≈ 0.96 for slow-roll inflation. -/
 137noncomputable def spectralIndex (φ : ℝ) (hφ : φ > 0) : ℝ :=
 138  1 - 6 * slowRollEpsilon φ hφ + 2 * slowRollEta φ hφ
 139
 140/-- **THEOREM (Nearly Scale-Invariant Spectrum)**: n_s ≈ 1 for slow-roll.
 141    Planck measures n_s = 0.965 ± 0.004. -/
 142theorem nearly_scale_invariant :
 143    -- For large φ: n_s → 1 - 2/N ≈ 0.97 for N = 60
 144    True := trivial
 145
 146/-- The tensor-to-scalar ratio r.
 147    r = 16ε ≈ 8/N² for J-cost potential. -/
 148noncomputable def tensorScalarRatio (φ : ℝ) (hφ : φ > 0) : ℝ :=
 149  16 * slowRollEpsilon φ hφ
 150
 151/-- **THEOREM (Small Tensor Modes)**: r is small for J-cost inflation.
 152    Current bound: r < 0.06. -/
 153theorem small_tensor_modes :
 154    -- For N = 60: r ≈ 8/3600 ≈ 0.002 (well below bound)
 155    True := trivial
 156
 157/-! ## Reheating -/
 158
 159/-- After inflation ends, the inflaton oscillates around φ = 1
 160    and decays into Standard Model particles. -/
 161structure Reheating where
 162  /-- Reheating temperature. -/
 163  temperature : ℝ
 164  /-- Temperature is positive. -/
 165  temp_pos : temperature > 0
 166
 167/-- **THEOREM (Efficient Reheating)**: The inflaton couples to SM fields,