phi_sq_lt

formal source

 218  have h2 : goldenRatio ^ 2 = goldenRatio + 1 := goldenRatio_sq
 219  linarith
 220
 221theorem phi_sq_lt : goldenRatio ^ 2 < (2.619 : ℝ) := by
 222  have h := phi_lt_16185
 223  have h2 : goldenRatio ^ 2 = goldenRatio + 1 := goldenRatio_sq
 224  linarith
 225
 226/-! ## φ^(-2) bounds (for quark masses) -/
 227
 228/-- φ^(-2) > 0.3818 (using φ² < 2.619) -/
 229theorem phi_neg2_gt : (0.3818 : ℝ) < goldenRatio ^ (-2 : ℤ) := by
 230  have h := phi_sq_lt  -- φ² < 2.619
 231  have hpos : (0 : ℝ) < goldenRatio ^ 2 := by positivity
 232  have heq : goldenRatio ^ (-2 : ℤ) = (goldenRatio ^ 2)⁻¹ :=
 233    zpow_neg_coe_of_pos goldenRatio (by norm_num : 0 < 2)
 234  rw [heq]
 235  have h1 : (0.3818 : ℝ) < 1 / (2.619 : ℝ) := by norm_num
 236  have h2 : 1 / (2.619 : ℝ) < 1 / goldenRatio ^ 2 :=
 237    one_div_lt_one_div_of_lt hpos h
 238  have h3 : 1 / goldenRatio ^ 2 = (goldenRatio ^ 2)⁻¹ := one_div _
 239  linarith
 240
 241/-- φ^(-2) < 0.382 (using φ² > 2.618) -/
 242theorem phi_neg2_lt : goldenRatio ^ (-2 : ℤ) < (0.382 : ℝ) := by
 243  have h := phi_sq_gt  -- 2.618 < φ²
 244  have hpos_bound : (0 : ℝ) < 2.618 := by norm_num
 245  have heq : goldenRatio ^ (-2 : ℤ) = (goldenRatio ^ 2)⁻¹ :=
 246    zpow_neg_coe_of_pos goldenRatio (by norm_num : 0 < 2)
 247  rw [heq]
 248  have h1 : (goldenRatio ^ 2)⁻¹ < (2.618 : ℝ)⁻¹ :=
 249    inv_strictAnti₀ hpos_bound h
 250  have h2 : (2.618 : ℝ)⁻¹ < (0.382 : ℝ) := by norm_num
 251  linarith