phiIntervalTight

formal source

  88  ⟨phi_gt_161803395, phi_lt_16180340⟩
  89
  90/-- Interval containing φ with tight bounds -/
  91def phiIntervalTight : Interval where
  92  lo := 161803395 / 100000000  -- 1.61803395
  93  hi := 16180340 / 10000000    -- 1.6180340
  94  valid := by norm_num
  95
  96/-- φ is contained in phiIntervalTight - PROVEN -/
  97theorem phi_in_phiIntervalTight : phiIntervalTight.contains goldenRatio := by
  98  simp only [Interval.contains, phiIntervalTight]
  99  constructor
 100  · have h := phi_gt_161803395
 101    have h1 : ((161803395 / 100000000 : ℚ) : ℝ) < goldenRatio := by
 102      calc ((161803395 / 100000000 : ℚ) : ℝ) = (1.61803395 : ℝ) := by norm_num
 103        _ < goldenRatio := h
 104    exact le_of_lt h1
 105  · have h := phi_lt_16180340
 106    have h1 : goldenRatio < ((16180340 / 10000000 : ℚ) : ℝ) := by
 107      calc goldenRatio < (1.6180340 : ℝ) := h
 108        _ = ((16180340 / 10000000 : ℚ) : ℝ) := by norm_num
 109    exact le_of_lt h1
 110
 111/-! ## Quarter-root bounds (needed for quarter/half-ladder rungs) -/
 112
 113/-- A certified lower rational bound for \(φ^{1/4}\). -/
 114noncomputable def phi_quarter_lo : ℝ := 1.12783847
 115
 116/-- A certified upper rational bound for \(φ^{1/4}\). -/
 117noncomputable def phi_quarter_hi : ℝ := 1.12783849
 118
 119lemma phi_quarter_lo_pow4_lt_phi_lo : phi_quarter_lo ^ (4 : ℕ) < (1.61803395 : ℝ) := by
 120  simp [phi_quarter_lo]
 121  norm_num