phiRing_comp_assoc
plain-language theorem explainer
Composition of morphisms between PhiRing objects is associative when viewed on their underlying carrier functions. Researchers constructing categorical models of Recognition Science algebras would cite this to confirm the category axioms hold for structures built around the golden element. The proof is a one-line term that reduces the claim to function extensionality and reflexivity on pointwise composition.
Claim. Let $A,B,C,D$ be commutative unital rings each equipped with a distinguished golden element. Let $f:A→B$, $g:B→C$, $h:C→D$ be ring homomorphisms that preserve addition, multiplication, negation, zero, one, and the golden element. Then the underlying map of the composite $h∘(g∘f)$ equals the underlying map of $(h∘g)∘f$.
background
PhiRing objects are commutative unital rings carrying a distinguished golden element phi together with its inverse witness. Morphisms are functions that preserve the full ring operations and send phi to phi. Composition of two such morphisms is defined by composing their underlying maps, as given in the definition of phiRing_comp.
proof idea
The proof applies function extensionality to reduce equality of maps to pointwise equality, after which reflexivity closes the goal because ordinary function composition is associative.
why it matters
This result verifies associativity of composition in the PhiRing category, a prerequisite for treating these algebraic structures as a category inside the Recognition Science framework. It parallels the corresponding associativity theorem for the recognition algebra category and supports any later constructions that invoke categorical composition of PhiRing morphisms. No open questions are resolved here.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.