r_prediction

formal source

 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
 178  have h_phi_lt : phi - 1 < 0.62 := by
 179    have h := phi_lt_onePointSixTwo
 180    linarith
 181  -- 0.61^4 ≈ 0.138 > 0.1, 0.62^4 ≈ 0.148 < 0.2
 182  have h_low : (0.61 : ℝ)^4 > 0.1 := by norm_num
 183  have h_high : (0.62 : ℝ)^4 < 0.2 := by norm_num
 184  have h_phi_pos : phi - 1 > 0 := by linarith [one_lt_phi]
 185  constructor
 186  · calc 0.1 < (0.61 : ℝ)^4 := h_low
 187       _ < (phi - 1)^4 := by
 188           apply pow_lt_pow_left₀ h_phi_gt (by norm_num) (by norm_num)
 189  · calc (phi - 1)^4 < (0.62 : ℝ)^4 := by
 190           apply pow_lt_pow_left₀ h_phi_lt (le_of_lt h_phi_pos) (by norm_num)
 191       _ < 0.2 := h_high
 192
 193/-! ## Running of the Spectral Index -/
 194
 195/-- The spectral index may "run" with scale: