phi_pos

formal source

  54def phi : ℝ := (1 + Real.sqrt 5) / 2
  55
  56/-- `φ` is positive. -/
  57theorem phi_pos : 0 < phi := by
  58  unfold phi
  59  have h5 : 0 ≤ Real.sqrt 5 := Real.sqrt_nonneg 5
  60  have : (0 : ℝ) < 1 + Real.sqrt 5 := by linarith
  61  linarith
  62
  63/-- `φ` is not zero. -/
  64theorem phi_ne_zero : phi ≠ 0 := ne_of_gt phi_pos
  65
  66/-- `φ > 1`. -/
  67theorem phi_gt_one : 1 < phi := by
  68  unfold phi
  69  have h5 : (2 : ℝ) ≤ Real.sqrt 5 := by
  70    have h4 : Real.sqrt 4 = 2 := by
  71      rw [show (4 : ℝ) = 2 ^ 2 from by norm_num]
  72      rw [Real.sqrt_sq (by norm_num : (0 : ℝ) ≤ 2)]
  73    calc (2 : ℝ) = Real.sqrt 4 := h4.symm
  74      _ ≤ Real.sqrt 5 := Real.sqrt_le_sqrt (by norm_num)
  75  linarith
  76
  77/-- `φ ≠ 1`. -/
  78theorem phi_ne_one : phi ≠ 1 := ne_of_gt phi_gt_one
  79
  80/-- The defining identity of the golden ratio: `φ² = φ + 1`. -/
  81theorem phi_sq_eq : phi ^ 2 = phi + 1 := by
  82  unfold phi
  83  have h5 : Real.sqrt 5 * Real.sqrt 5 = 5 :=
  84    Real.mul_self_sqrt (by norm_num : (5 : ℝ) ≥ 0)
  85  have : ((1 + Real.sqrt 5) / 2) ^ 2 = (1 + Real.sqrt 5) / 2 + 1 := by
  86    field_simp
  87    nlinarith [h5]