`phi_gt_one`

proved

show as: view math explainer →

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

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.Derivations.MassToLight on GitHub at line 64.

browse module

All declarations in this module, on Recognition.

explainer page

A cached Ask Recognition explainer exists for this declaration.

open explainer

formal source

  61
  62/-! ## Geometric Bounds Helper -/
  63
  64lemma phi_gt_one : phi > 1 := by
  65  unfold phi
  66  have : Real.sqrt 5 > 1 := by
  67    rw [← Real.sqrt_one]
  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)]

papers checked against this theorem

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