`phi17_gt`

proved

show as: view math explainer →

module: IndisputableMonolith.Masses.Verification
domain: Masses
line: 199 · github
papers citing: none yet

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.Masses.Verification on GitHub at line 199.

browse module

All declarations in this module, on Recognition.

explainer page

A cached Ask Recognition explainer exists for this declaration.

open explainer

depends on

used by

formal source

 196    _ < (46.99 : ℝ) * (4.237 : ℝ) := by nlinarith
 197    _ < (200 : ℝ) := by norm_num
 198
 199private lemma phi17_gt : (3569 : ℝ) < Constants.phi ^ (17 : ℕ) := by
 200  rw [phi_eq_goldenRatio]
 201  have h8_lo := Numerics.phi_pow8_gt
 202  have hφ_lo := Numerics.phi_gt_1618
 203  have hpos8 : (0 : ℝ) < Real.goldenRatio ^ 8 := by positivity
 204  have hpos16 : (0 : ℝ) < Real.goldenRatio ^ 8 * Real.goldenRatio ^ 8 := by positivity
 205  have heq : Real.goldenRatio ^ 17 = Real.goldenRatio ^ 8 * Real.goldenRatio ^ 8 * Real.goldenRatio := by ring_nf
 206  rw [heq]
 207  have h16_lo : (46.97 : ℝ) * (46.97 : ℝ) < Real.goldenRatio ^ 8 * Real.goldenRatio ^ 8 :=
 208    mul_lt_mul h8_lo (le_of_lt h8_lo) (by norm_num) (le_of_lt hpos8)
 209  have h17_lo : (46.97 : ℝ) * (46.97 : ℝ) * (1.618 : ℝ) <
 210      Real.goldenRatio ^ 8 * Real.goldenRatio ^ 8 * Real.goldenRatio :=
 211    mul_lt_mul h16_lo (le_of_lt hφ_lo) (by norm_num) (le_of_lt hpos16)
 212  linarith [show (3569 : ℝ) < (46.97 : ℝ) * (46.97 : ℝ) * (1.618 : ℝ) from by norm_num]
 213
 214private lemma phi17_lt : Constants.phi ^ (17 : ℕ) < (3574 : ℝ) := by
 215  rw [phi_eq_goldenRatio]
 216  have h8_hi := Numerics.phi_pow8_lt
 217  have hφ_hi := Numerics.phi_lt_16185
 218  have hpos8 : (0 : ℝ) < Real.goldenRatio ^ 8 := by positivity
 219  have hφ_pos : (0 : ℝ) < Real.goldenRatio := by simpa using Real.goldenRatio_pos
 220  have heq : Real.goldenRatio ^ 17 = Real.goldenRatio ^ 8 * Real.goldenRatio ^ 8 * Real.goldenRatio := by ring_nf
 221  rw [heq]
 222  have h16_hi : Real.goldenRatio ^ 8 * Real.goldenRatio ^ 8 < (46.99 : ℝ) * (46.99 : ℝ) :=
 223    mul_lt_mul h8_hi (le_of_lt h8_hi) hpos8 (by norm_num)
 224  have h17_hi : Real.goldenRatio ^ 8 * Real.goldenRatio ^ 8 * Real.goldenRatio <
 225      (46.99 : ℝ) * (46.99 : ℝ) * (1.6185 : ℝ) :=
 226    mul_lt_mul h16_hi (le_of_lt hφ_hi) hφ_pos (by norm_num)
 227  linarith [show (46.99 : ℝ) * (46.99 : ℝ) * (1.6185 : ℝ) < (3574 : ℝ) from by norm_num]
 228
 229theorem muon_ratio_undershoot :

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.