`phi11_lt`

proved

show as: view math explainer →

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

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.Masses.Verification on GitHub at line 187.

browse module

All declarations in this module, on Recognition.

explainer page

Tracked in the explainer inventory; generation is lazy so crawlers do not trigger LLM jobs.

open explainer

depends on

used by

formal source

 184    _ < Real.goldenRatio ^ 8 * (4.236 : ℝ) := by nlinarith
 185    _ < Real.goldenRatio ^ 8 * Real.goldenRatio ^ 3 := by nlinarith
 186
 187private lemma phi11_lt : Constants.phi ^ (11 : ℕ) < (200 : ℝ) := by
 188  rw [phi_eq_goldenRatio]
 189  have h8 := Numerics.phi_pow8_lt
 190  have h3 := Numerics.phi_cubed_lt
 191  have hpos : (0 : ℝ) < Real.goldenRatio ^ 3 := by positivity
 192  have heq : Real.goldenRatio ^ 11 = Real.goldenRatio ^ 8 * Real.goldenRatio ^ 3 := by ring_nf
 193  rw [heq]
 194  calc Real.goldenRatio ^ 8 * Real.goldenRatio ^ 3
 195      < (46.99 : ℝ) * Real.goldenRatio ^ 3 := by nlinarith
 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

papers checked against this theorem

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