phi_psi_diff

formal source

 102  unfold φ ψ; ring
 103
 104/-- **THEOREM: φ − ψ = √5** -/
 105theorem phi_psi_diff : φ - ψ = Real.sqrt 5 := by
 106  unfold φ ψ; ring
 107
 108/-- **THEOREM: φ⁻¹ = φ − 1** -/
 109theorem phi_inv : φ⁻¹ = φ - 1 := by
 110  unfold φ
 111  have hden : ((1 + Real.sqrt 5) / 2 : ℝ) ≠ 0 := by
 112    have hφ : 0 < ((1 + Real.sqrt 5) / 2 : ℝ) := by
 113      have h := sqrt5_pos
 114      linarith
 115    exact ne_of_gt hφ
 116  have h5 : Real.sqrt 5 ^ 2 = 5 := Real.sq_sqrt (by norm_num : (5 : ℝ) ≥ 0)
 117  field_simp [hden]
 118  nlinarith [h5]
 119
 120/-! ## §2. Elements of ℤ[φ] -/
 121
 122/-- An element of ℤ[φ] is a pair (a, b) representing a + bφ. -/
 123@[ext]
 124structure PhiInt where
 125  /-- The "rational" part -/
 126  a : ℤ
 127  /-- The "φ" part -/
 128  b : ℤ
 129deriving DecidableEq, Repr
 130
 131/-- Interpret a PhiInt as a real number: a + bφ -/
 132noncomputable def PhiInt.toReal (z : PhiInt) : ℝ := z.a + z.b * φ
 133
 134/-- Zero element: 0 + 0·φ = 0 -/
 135def PhiInt.zero : PhiInt := ⟨0, 0⟩