r_in_detectable_range

formal source

  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:
  83    Ω₀ = 2π / ln(1/X_opt) = 2π / ln(π/φ).
  84    Numerically: π/φ ≈ 1.942, ln(1.942) ≈ 0.664, so Ω₀ ≈ 9.47.
  85
  86    This produces oscillations in the primordial power spectrum
  87    with period Δln(k) = 2π/Ω₀ ≈ 0.664. -/
  88noncomputable def Omega_0 : ℝ := 2 * Real.pi / Real.log (Real.pi / phi)
  89
  90/-- Ω₀ is positive (π/φ > 1, so ln(π/φ) > 0). -/
  91theorem Omega_0_pos : 0 < Omega_0 := by
  92  unfold Omega_0
  93  apply div_pos (mul_pos (by norm_num) Real.pi_pos)
  94  apply Real.log_pos
  95  rw [one_lt_div phi_pos]
  96  exact lt_of_lt_of_le (by linarith [phi_lt_two]) (le_of_lt Real.pi_gt_three)
  97