`phi_lt_two`

proved

show as: view math explainer →

module: IndisputableMonolith.Derivations.MassToLight
domain: Derivations
line: 71 · github
papers citing: none yet

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.Derivations.MassToLight on GitHub at line 71.

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

  68    exact Real.sqrt_lt_sqrt (by norm_num) (by norm_num)
  69  linarith
  70
  71lemma phi_lt_two : phi < 2 := by
  72  unfold phi
  73  have : Real.sqrt 5 < 3 := by
  74    rw [← Real.sqrt_sq (by norm_num : (0:ℝ)≤3)]
  75    apply Real.sqrt_lt_sqrt (by norm_num) (by norm_num)
  76  linarith
  77
  78/-! ## Specific Powers -/
  79
  80/-- Lower bound for φ. -/
  81lemma phi_gt_1_6 : phi > 1.6 := by
  82  unfold phi
  83  norm_num
  84  have : Real.sqrt 5 > 2.2 := by
  85    rw [← Real.sqrt_sq (by norm_num : (0:ℝ)≤2.2)]
  86    apply Real.sqrt_lt_sqrt (by norm_num) (by norm_num)
  87  linarith
  88
  89/-- Upper bound for φ. -/
  90lemma phi_lt_1_7 : phi < 1.7 := by
  91  unfold phi
  92  norm_num
  93  have : Real.sqrt 5 < 2.4 := by
  94    rw [← Real.sqrt_sq (by norm_num : (0:ℝ)≤2.4)]
  95    apply Real.sqrt_lt_sqrt (by norm_num) (by norm_num)
  96  linarith
  97
  98/-- φ¹⁰ > 100. -/
  99theorem phi_10_bounds : phi_power 10 > 100 := by
 100  unfold phi_power
 101  have h : phi > 1.6 := phi_gt_1_6

papers checked against this theorem

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