IsSelfSimilar

formal source

  20/-! ## Self-Similarity Definition -/
  21
  22/-- A ratio r is self-similar if r² = r + 1. -/
  23def IsSelfSimilar (r : ℝ) : Prop := r^2 = r + 1
  24
  25/-- The golden ratio is positive -/
  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