phiPow

formal source

 418    These form the **φ-ladder** — the fundamental scale structure of RS.
 419
 420    Key property: φⁿ ∈ ℤ[φ] for all n ∈ ℤ. -/
 421noncomputable def phiPow (n : ℤ) : PhiInt :=
 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 ℤ[φ].** -/
 438theorem phiInt_sq : PhiInt.phi * PhiInt.phi = PhiInt.phi + PhiInt.one := by
 439  ext
 440  · change 0 * 0 + 1 * 1 = 0 + 1
 441    norm_num
 442  · change 0 * 1 + 1 * 0 + 1 * 1 = 1 + 0
 443    norm_num
 444
 445/-! ## §7. Connection to Cost Algebra -/
 446
 447/-- **Key bridge**: J(φ) in the cost algebra.
 448    J(φ) = ½(φ + φ⁻¹) − 1 = ½(φ + φ−1) − 1 = ½·√5 − 1 ≈ 0.118
 449
 450    This is the **coherence cost of self-similarity** — the minimum nonzero
 451    cost in the φ-ladder. -/