tensorScalarRatio

formal source

 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,
 168    allowing efficient energy transfer after inflation. -/
 169theorem efficient_reheating :
 170    -- Oscillations around φ = 1 decay into particles
 171    True := trivial
 172
 173/-! ## The RS Interpretation -/
 174
 175/-- In RS, inflation is the universe "rolling down" the J-cost landscape:
 176
 177    1. Initial conditions: φ >> 1 (high cost, far from equilibrium)
 178    2. Slow roll: The field slowly approaches equilibrium