alpha_attractor_bounds

formal source

  38
  39theorem alpha_attractor_pos : 0 < alpha_attractor := pow_pos phi_pos 2
  40
  41theorem alpha_attractor_bounds : 2.5 < alpha_attractor ∧ alpha_attractor < 2.7 :=
  42  phi_squared_bounds
  43
  44/-! ## Spectral Predictions -/
  45
  46/-- Spectral index: n_s ≈ 1 - 2/N (standard slow-roll result). -/
  47noncomputable def spectral_index (N : ℝ) : ℝ := 1 - 2 / N
  48
  49/-- Tensor-to-scalar ratio: r ≈ 12α/N² = 12φ²/N².
  50    This is the RS-SPECIFIC prediction: the standard α-attractor formula
  51    with α = φ² (not a free parameter). -/
  52noncomputable def tensor_to_scalar (N : ℝ) : ℝ := 12 * alpha_attractor / N ^ 2
  53
  54/-- For N = 55 e-foldings: r ≈ 12 * 2.618 / 3025 ≈ 0.0104. -/
  55theorem r_at_55_bounds : tensor_to_scalar 55 > 0 := by
  56  unfold tensor_to_scalar
  57  apply div_pos
  58  · exact mul_pos (by norm_num) alpha_attractor_pos
  59  · positivity
  60
  61/-- For N = 55: n_s ≈ 0.964. -/
  62theorem n_s_at_55 : 0.96 < spectral_index 55 ∧ spectral_index 55 < 0.97 := by
  63  unfold spectral_index; constructor <;> norm_num
  64
  65/-- The tensor ratio r is in the range detectable by LiteBIRD/CMB-S4.
  66    For α = φ² and N ∈ [50, 60]: r ∈ (0.005, 0.02). -/
  67theorem r_in_detectable_range :
  68    tensor_to_scalar 60 > 0 ∧ tensor_to_scalar 50 > 0 := by
  69  unfold tensor_to_scalar
  70  constructor <;> (apply div_pos (mul_pos (by norm_num : (0:ℝ) < 12) alpha_attractor_pos)
  71                    (by positivity))