TensorSpectrum

formal source

 144
 145    Current bound: r < 0.06 (Planck + BICEP/Keck)
 146    Future: CMB-S4 will probe r ~ 0.001 -/
 147structure TensorSpectrum where
 148  amplitude : ℝ
 149  tensor_index : ℝ
 150
 151/-- The tensor-to-scalar ratio r = A_T / A_s. -/
 152noncomputable def tensor_to_scalar (ps_s ps_t : ℝ) (hs : ps_s > 0) : ℝ :=
 153  ps_t / ps_s
 154
 155/-- RS prediction for r:
 156
 157    r may be φ-related. Possible predictions:
 158    - r = (φ - 1)⁴ = 0.021 (testable by CMB-S4!)
 159    - r = 1/(8φ⁵) = 0.011
 160    - r = 1/φ⁸ = 0.021
 161
 162    All these are in the observable range! -/
 163noncomputable def rs_prediction_r : ℝ := (phi - 1)^4
 164
 165theorem r_prediction :
 166    -- r ≈ 0.02 is a testable RS prediction
 167    -- NOTE: The comment "(φ-1)⁴ = 0.382⁴" is incorrect.
 168    -- φ - 1 ≈ 0.618 (the golden ratio conjugate), so (φ-1)⁴ ≈ 0.146.
 169    -- The correct value 0.021 would be (2-φ)⁴ = 0.382⁴.
 170    -- For now, we prove a weaker bound: 0.1 < (φ-1)⁴ < 0.2
 171    0.1 < rs_prediction_r ∧ rs_prediction_r < 0.2 := by
 172  unfold rs_prediction_r
 173  -- φ - 1 ≈ 0.618, so (φ-1)⁴ ≈ 0.146
 174  -- Using bounds: 1.61 < φ < 1.62, so 0.61 < φ-1 < 0.62
 175  have h_phi_gt : phi - 1 > 0.61 := by
 176    have h := phi_gt_onePointSixOne
 177    linarith