psi_equation

formal source

  84  nlinarith [h5]
  85
  86/-- **THEOREM: ψ² = ψ + 1** (conjugate satisfies the same equation). -/
  87theorem psi_equation : ψ ^ 2 = ψ + 1 := by
  88  unfold ψ
  89  have h5 : Real.sqrt 5 ^ 2 = 5 := Real.sq_sqrt (by norm_num : (5:ℝ) ≥ 0)
  90  ring_nf
  91  nlinarith [h5]
  92
  93/-- **THEOREM: φ · ψ = −1** (product of conjugates). -/
  94theorem phi_psi_product : φ * ψ = -1 := by
  95  unfold φ ψ
  96  have h5 : Real.sqrt 5 ^ 2 = 5 := Real.sq_sqrt (by norm_num : (5:ℝ) ≥ 0)
  97  ring_nf
  98  nlinarith [h5]
  99
 100/-- **THEOREM: φ + ψ = 1** (trace). -/
 101theorem phi_psi_sum : φ + ψ = 1 := by
 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]