phiPow

proof body

Definition body.

 422  if n = 0 then ⟨1, 0⟩
 423  else if n = 1 then ⟨0, 1⟩
 424  else if n > 1 then
 425    -- φⁿ = φⁿ⁻¹ + φⁿ⁻² (Fibonacci recurrence in ℤ[φ])
 426    -- Build iteratively
 427    let rec build : ℕ → PhiInt × PhiInt
 428      | 0 => (⟨1, 0⟩, ⟨0, 1⟩)  -- (φ⁰, φ¹)
 429      | k + 1 =>
 430        let (prev, curr) := build k
 431        (curr, curr + prev)  -- (φⁿ, φⁿ⁺¹ = φⁿ + φⁿ⁻¹)
 432    (build (n.toNat - 1)).2
 433  else
 434    -- For negative n: φ⁻¹ = φ − 1, so φ⁻ⁿ = conjugation-related
 435    ⟨0, 0⟩  -- Placeholder for negative powers
 436
 437/-- **THEOREM: φ² = φ + 1 in ℤ[φ].** -/