theorem
proved
tactic proof
r_prediction
show as:
view Lean formalization →
formal statement (Lean)
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
proof body
Tactic-mode proof.
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:
196
197 dn_s / d ln k ≈ -0.006 ± 0.007 (Planck 2018)
198
199 Consistent with zero, but RS may predict specific value.
200
201 If spectral index is φ-quantized, running may show φ-structure. -/