canonicalPhiRingObj
plain-language theorem explainer
The declaration packages the ring of integers adjoined with the golden ratio as the canonical object in the PhiRing category. Algebraic layer constructions in Recognition Science cite it when assembling the phi component of multi-layer systems. The definition simply instantiates the PhiRingObj structure by delegating every field to the already-verified operations and relation on PhiInt.
Claim. The canonical object of the Phi-ring category is the ring $ℤ[φ]$ equipped with its standard addition, multiplication, additive inverse, unit, zero, distinguished element $φ$, and multiplicative inverse $φ^{-1}$, satisfying the relation $φ^2 = φ + 1$.
background
PhiRingObj is the structure that encodes a commutative unital ring together with a distinguished golden element $φ$ and a witness for its multiplicative inverse, plus the full set of ring axioms. The module Algebra.RecognitionCategory collects these algebraic layers to support higher Recognition Science constructions that combine cost, phi, ledger, and octave data. Upstream, the theorem phiInt_sq proves the minimal polynomial relation $φ^2 = φ + 1$ inside $ℤ[φ]$ by direct verification on the basis elements 1 and $φ$.
proof idea
The definition is a direct structure instantiation: Carrier is set to PhiRing.PhiInt and every subsequent field (zero, one, add, mul, phi, phiInv, and all axioms) is assigned the corresponding operation or theorem from PhiRing.PhiInt, with the phi_relation field supplied by the upstream theorem phiInt_sq.
why it matters
This definition supplies the phiLayer field inside canonicalLayerSysPlus, the canonical linked system that assembles cost, phi, ledger, and octave layers. It realizes the self-similar fixed point $φ$ required by forcing-chain step T6 and supplies the algebraic carrier needed for Recognition Composition Law applications. No open scaffolding remains at this node.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.