phi_gt_one

formal source

  26theorem phi_pos : φ > 0 := Constants.phi_pos
  27
  28/-- The golden ratio is greater than 1 -/
  29theorem phi_gt_one : φ > 1 := Constants.one_lt_phi
  30
  31/-! ## φ Satisfies Self-Similarity -/
  32
  33/-- **THEOREM**: The golden ratio satisfies r² = r + 1. -/
  34theorem phi_is_self_similar : IsSelfSimilar φ := Constants.phi_sq_eq
  35
  36/-- The conjugate ratio (1 - √5)/2 also satisfies r² = r + 1 -/
  37noncomputable def φ_conjugate : ℝ := (1 - Real.sqrt 5) / 2
  38
  39theorem phi_conjugate_self_similar : IsSelfSimilar φ_conjugate := by
  40  unfold IsSelfSimilar φ_conjugate
  41  have h5 : Real.sqrt 5 ≥ 0 := Real.sqrt_nonneg 5
  42  have h_sq : Real.sqrt 5 ^ 2 = 5 := Real.sq_sqrt (by norm_num : (5 : ℝ) ≥ 0)
  43  ring_nf
  44  rw [h_sq]
  45  ring
  46
  47/-- The conjugate is negative -/
  48theorem phi_conjugate_neg : φ_conjugate < 0 := by
  49  unfold φ_conjugate
  50  have h : Real.sqrt 5 > 1 := by
  51    have h1 : Real.sqrt 5 ^ 2 = 5 := Real.sq_sqrt (by norm_num : (5 : ℝ) ≥ 0)
  52    nlinarith [Real.sqrt_nonneg 5, sq_nonneg (Real.sqrt 5 - 1)]
  53  linarith
  54
  55/-! ## Uniqueness of φ -/
  56
  57/-- **THEOREM**: φ is the unique positive solution to r² = r + 1. -/
  58theorem phi_unique_positive : ∀ r : ℝ, r > 0 → IsSelfSimilar r → r = φ := by
  59  intro r hr h_self