phi_equation

formal source

  77  linarith
  78
  79/-- **THEOREM: φ² = φ + 1** (the defining equation). -/
  80theorem phi_equation : φ ^ 2 = φ + 1 := by
  81  unfold φ
  82  have h5 : Real.sqrt 5 ^ 2 = 5 := Real.sq_sqrt (by norm_num : (5:ℝ) ≥ 0)
  83  ring_nf
  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 φ