theorem
proved
tactic proof
rs_params_perturbative_proven
show as:
view Lean formalization →
formal statement (Lean)
131theorem rs_params_perturbative_proven : |alpha_from_phi * cLag_from_phi| < 0.1 := by
proof body
Tactic-mode proof.
132 have hα_pos := rs_params_positive.1
133 have hC_pos := rs_params_positive.2
134 rw [abs_of_nonneg (mul_nonneg (le_of_lt hα_pos) (le_of_lt hC_pos))]
135 have hα_lt : alpha_from_phi < 1 / 2 := alpha_lt_half
136 have hC_lt : cLag_from_phi < 1 / 10 := cLag_lt_one_tenth
137 calc alpha_from_phi * cLag_from_phi
138 < (1 / 2) * (1 / 10) := by
139 apply mul_lt_mul'' hα_lt hC_lt (le_of_lt hα_pos) (le_of_lt hC_pos)
140 _ = 1 / 20 := by norm_num
141 _ < 0.1 := by norm_num
142
143/-- STATUS: Product < 0.02 needs tighter bounds.
144
145 PROGRESS: Proven product < 0.05 (since α < 1/2, C_lag < 1/10)
146 NEEDED: Either α < 1/5 OR C_lag < 1/11 to get product < 0.02
147
148 Current bounds:
149 - α = (1-1/φ)/2 where φ = (1+√5)/2
150 - Need to show α < 1/5 OR find tighter C_lag bound
151
152 Path forward:
153 - Prove φ < 1.62 ⟹ 1/φ > 0.617 ⟹ 1-1/φ < 0.383 ⟹ α < 0.192 < 1/5 ✓
154 - Requires proving √5 < 2.24 ⟹ φ < (1+2.24)/2 = 1.62
155 - This is doable with Mathlib's Real.sqrt inequalities
156-/