phi_pow58_lt

formal source

 651    _ < goldenRatio ^ 54 * goldenRatio ^ 4 := by nlinarith
 652
 653/-- φ^58 < 1.324e12 (using φ^54 < 192983018016 and φ^4 < 6.86) -/
 654theorem phi_pow58_lt : goldenRatio ^ 58 < (1.324e12 : ℝ) := by
 655  rw [phi_pow58_eq]
 656  have h54 := phi_pow54_lt  -- φ^54 < 192983018016
 657  have h4 := phi_pow4_lt    -- φ^4 < 6.86
 658  have hpos54 : (0 : ℝ) < goldenRatio ^ 54 := by positivity
 659  have hpos4 : (0 : ℝ) < goldenRatio ^ 4 := by positivity
 660  calc goldenRatio ^ 54 * goldenRatio ^ 4 < (192983018016 : ℝ) * goldenRatio ^ 4 := by nlinarith
 661    _ < (192983018016 : ℝ) * (6.86 : ℝ) := by nlinarith
 662    _ < (1.324e12 : ℝ) := by norm_num
 663
 664/-! ## φ^(-58) bounds (for neutrino mass predictions) -/
 665
 666/-- φ^(-58) > 7.55e-13 (using φ^58 < 1.324e12) -/
 667theorem phi_neg58_gt : (7.55e-13 : ℝ) < goldenRatio ^ (-58 : ℤ) := by
 668  have h := phi_pow58_lt  -- φ^58 < 1.324e12
 669  have hpos : (0 : ℝ) < goldenRatio ^ 58 := by positivity
 670  have heq : goldenRatio ^ (-58 : ℤ) = (goldenRatio ^ 58)⁻¹ :=
 671    zpow_neg_coe_of_pos goldenRatio (by norm_num : 0 < 58)
 672  rw [heq]
 673  have h1 : (7.55e-13 : ℝ) < 1 / (1.324e12 : ℝ) := by norm_num
 674  have h2 : 1 / (1.324e12 : ℝ) < 1 / goldenRatio ^ 58 :=
 675    one_div_lt_one_div_of_lt hpos h
 676  have h3 : 1 / goldenRatio ^ 58 = (goldenRatio ^ 58)⁻¹ := one_div _
 677  linarith
 678
 679/-- φ^(-58) < 7.57e-13 (using φ^58 > 1.3219e12) -/
 680theorem phi_neg58_lt : goldenRatio ^ (-58 : ℤ) < (7.57e-13 : ℝ) := by
 681  have h := phi_pow58_gt  -- 1.3219e12 < φ^58
 682  have hpos_bound : (0 : ℝ) < 1.3219e12 := by norm_num
 683  have heq : goldenRatio ^ (-58 : ℤ) = (goldenRatio ^ 58)⁻¹ :=
 684    zpow_neg_coe_of_pos goldenRatio (by norm_num : 0 < 58)