def
definition
phiInterval
show as:
view math explainer →
open explainer
Generate a durable explainer page for this declaration.
open lean source
IndisputableMonolith.Numerics.Interval.Pow on GitHub at line 50.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
47 ⟨h_lo, h_hi⟩
48
49/-- Interval containing φ = (1 + √5)/2 ≈ 1.618 -/
50def phiInterval : Interval where
51 lo := 1618 / 1000
52 hi := 1619 / 1000
53 valid := by norm_num
54
55/-- φ is in phiInterval - PROVEN using sqrt bounds -/
56theorem phi_in_phiInterval : phiInterval.contains ((1 + Real.sqrt 5) / 2) := by
57 simp only [Interval.contains, phiInterval]
58 constructor
59 · have h := phi_gt_1618
60 have h1 : ((1618 / 1000 : ℚ) : ℝ) < (1 + Real.sqrt 5) / 2 := by
61 calc ((1618 / 1000 : ℚ) : ℝ) = (1.618 : ℝ) := by norm_num
62 _ < (1 + Real.sqrt 5) / 2 := h
63 exact le_of_lt h1
64 · have h := phi_lt_16185
65 have h1 : (1 + Real.sqrt 5) / 2 < ((1619 / 1000 : ℚ) : ℝ) := by
66 calc (1 + Real.sqrt 5) / 2 < (1.6185 : ℝ) := h
67 _ < (1.619 : ℝ) := by norm_num
68 _ = ((1619 / 1000 : ℚ) : ℝ) := by norm_num
69 exact le_of_lt h1
70
71/-- φ = (1 + √5)/2 (Mathlib definition) -/
72theorem phi_eq_formula : goldenRatio = (1 + Real.sqrt 5) / 2 := rfl
73
74/-- φ^(-5) interval ≈ 0.0902 - PROVEN using φ⁻⁵ = (φ⁻¹)⁵ -/
75def phi_pow_neg5_interval : Interval where
76 lo := 89 / 1000 -- Matches phi_inv5_interval_proven
77 hi := 91 / 1000
78 valid := by norm_num
79
80theorem phi_pow_neg5_in_interval : phi_pow_neg5_interval.contains (((1 + Real.sqrt 5) / 2) ^ (-5 : ℝ)) := by