phiInt_sq
plain-language theorem explainer
Algebraists formalizing quadratic integer rings cite the result that φ satisfies φ² = φ + 1 inside ℤ[φ]. Recognition Science modelers invoke it to anchor the self-similar fixed point on the phi-ladder. The proof reduces equality to componentwise arithmetic on the pair representation of PhiInt and confirms the identities by normalization.
Claim. In the ring ℤ[φ] whose elements are pairs (a, b) ∈ ℤ × ℤ interpreted as a + bφ, the equality φ · φ = φ + 1 holds.
background
PhiInt is the structure whose elements are pairs (a, b) with a, b ∈ ℤ, interpreted via toReal as a + bφ. The module Algebra.PhiRing equips this carrier with ring operations to support the Recognition framework's cost algebra and forcing chain. Upstream lemmas supply the integer one from IntegersFromLogic and the J-cost from MultiplicativeRecognizerL4 and ObserverForcing, which together calibrate the coherence cost J(φ) = ½(φ + φ⁻¹) − 1.
proof idea
The proof applies the extensionality lemma for PhiInt, reducing the ring equality to two component equations. It rewrites multiplication and addition on the integer coefficients, then invokes norm_num to verify 0·0 + 1·1 = 0 + 1 and 0·1 + 1·0 + 1·1 = 1 + 0.
why it matters
This theorem supplies the defining relation required by the downstream phi_ring_certificate, which lists φ² = φ + 1 among the verified ring axioms. It directly instantiates the self-similar fixed point (T6) and the eight-tick octave structure in the forcing chain, enabling the phi-ladder mass formula and the canonical object in RecognitionCategory.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.