phi_pos

formal source

  82noncomputable abbrev φ : ℝ := Constants.phi
  83
  84/-- φ is positive -/
  85theorem phi_pos : φ > 0 := Constants.phi_pos
  86
  87/-- φ > 1 -/
  88theorem phi_gt_one : φ > 1 := Constants.one_lt_phi
  89
  90/-- 1/φ = φ - 1 (the golden ratio property) -/
  91theorem phi_inv : 1 / φ = φ - 1 := by
  92  have hsq : φ ^ 2 = φ + 1 := Constants.phi_sq_eq
  93  have hpos : 0 < φ := Constants.phi_pos
  94  have hne : φ ≠ 0 := hpos.ne'
  95  have hmul : φ * (φ - 1) = 1 := by
  96    calc
  97      φ * (φ - 1) = φ ^ 2 - φ := by ring
  98      _ = (φ + 1) - φ := by simp [hsq]
  99      _ = 1 := by ring
 100  have hdiv : φ - 1 = 1 / φ := by
 101    apply (eq_div_iff hne).2
 102    simpa [mul_comm, mul_left_comm, mul_assoc] using hmul
 103  exact hdiv.symm
 104
 105/-- φ² = φ + 1 (the defining equation) -/
 106theorem phi_sq : φ^2 = φ + 1 := Constants.phi_sq_eq
 107
 108/-- φ + 1/φ = √5 -/
 109theorem phi_plus_inv : φ + 1/φ = Real.sqrt 5 := by
 110  unfold φ Constants.phi
 111  have hroot_pos : (0 : ℝ) < 5 := by norm_num
 112  have hroot_ne : Real.sqrt 5 + 1 ≠ 0 := by
 113    have := Real.sqrt_nonneg 5
 114    linarith
 115  field_simp