tensor_to_scalar

formal source

  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))
  72
  73/-! ## Log-Periodic Modulation -/
  74
  75/-- The optimal recognition ratio: X_opt = φ/π.
  76    This is the ratio at which recognition cost and geometric constraint
  77    are in balance. -/
  78noncomputable def X_opt : ℝ := phi / Real.pi
  79
  80theorem X_opt_pos : 0 < X_opt := div_pos phi_pos Real.pi_pos
  81
  82/-- The log-periodic modulation frequency: