phiInt_sq

formal source

 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. -/
 452theorem J_at_phi : CostAlgebra.J φ = (Real.sqrt 5 - 2) / 2 := by
 453  unfold CostAlgebra.J Cost.Jcost φ
 454  have hφ : (1 + Real.sqrt 5) / 2 ≠ 0 := ne_of_gt phi_pos
 455  have h5 : Real.sqrt 5 ^ 2 = 5 := Real.sq_sqrt (by norm_num : (5:ℝ) ≥ 0)
 456  field_simp [hφ]
 457  nlinarith [h5, sqrt5_pos]
 458
 459/-! ## §8. Summary -/
 460
 461/-- **φ-RING CERTIFICATE**
 462
 463    ℤ[φ] has been formalized with:
 464    1. Ring operations (add, mul, neg) ✓
 465    2. Ring axioms (comm, assoc, distrib, identities) ✓
 466    3. Galois conjugation σ (involution, ring homomorphism) ✓
 467    4. Norm form N(a+bφ) = a²+ab−b² (multiplicative) ✓
 468    5. φ² = φ + 1 (defining relation) ✓