PhiRingObj
plain-language theorem explainer
The structure packages data for a commutative unital ring equipped with a distinguished element phi satisfying the golden-ratio equation phi squared equals phi plus one together with a two-sided multiplicative inverse. Algebraists building Recognition Science layer systems cite it when assembling the category whose objects carry the phi fixed point. The declaration is a plain structure definition with no proof body or computational content.
Claim. A phi-ring object consists of a carrier set $C$ with operations $0,1,+,−,⋅$ making $(C,0,1,+,−,⋅)$ a commutative ring with unit, together with an element $ϕ∈C$ and an element $ϕ^{−1}∈C$ satisfying $ϕ⋅ϕ^{−1}=1=ϕ^{−1}⋅ϕ$ and $ϕ^{2}=ϕ+1$.
background
Recognition Science places algebraic objects inside a category whose morphisms preserve ring operations and the distinguished golden element. The structure therefore records a carrier type, the six ring operations, the element phi, its inverse phiInv, and the full list of ring axioms plus the two inverse equations and the quadratic relation. Upstream arithmetic results supply the associativity, commutativity, and identity laws that are simply redeclared as fields here. The local module imports CostAlgebra, PhiRing, LedgerAlgebra and OctaveAlgebra, indicating that phi-ring objects are intended to sit alongside cost families and octave layers in composite systems.
proof idea
The declaration is a structure definition; no proof is required. Each field is declared directly: the carrier and operations, followed by the ten ring axioms, the two inverse equations, and the quadratic relation phi phi = phi + one.
why it matters
PhiRingObj supplies the objects of the paper-facing PhiRing category and is instantiated by canonicalPhiRingObj as the ring of integers adjoined with phi. It is required by LayerSysPlusObj to package the phi layer with cost, ledger and octave layers under the bridge axioms B1 and B2. The quadratic relation directly encodes the self-similar fixed point forced at step T6 of the unified forcing chain, while the inverse witness realises the phiInv element used in Recognition Composition Law identities.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.