`phi_gt_1_6`

proved

show as: view math explainer →

module: IndisputableMonolith.Support.PhiApprox
domain: Support
line: 20 · github
papers citing: none yet

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.Support.PhiApprox on GitHub at line 20.

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

  17  rw [← Real.sqrt_sq h2_4_pos]
  18  exact Real.sqrt_lt_sqrt h5_pos h
  19
  20private lemma phi_gt_1_6 : (1.6 : ℝ) < Constants.phi := by
  21  unfold Constants.phi
  22  have h : (1.6 : ℝ) = (1 + 2.2) / 2 := by norm_num
  23  rw [h]
  24  apply div_lt_div_of_pos_right _ (by norm_num : (0 : ℝ) < 2)
  25  linarith [sqrt5_gt_2_2]
  26
  27private lemma phi_lt_1_7 : Constants.phi < (1.7 : ℝ) := by
  28  unfold Constants.phi
  29  have h : (1.7 : ℝ) = (1 + 2.4) / 2 := by norm_num
  30  rw [h]
  31  apply div_lt_div_of_pos_right _ (by norm_num : (0 : ℝ) < 2)
  32  linarith [sqrt5_lt_2_4]
  33
  34/-- Coarse bounds on φ used by downstream numerics modules. -/
  35theorem phi_bounds_stub : (1.6 : ℝ) < Constants.phi ∧ Constants.phi < 1.7 :=
  36  ⟨phi_gt_1_6, phi_lt_1_7⟩
  37
  38end Support
  39end IndisputableMonolith

papers checked against this theorem

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