phiRing_comp_assoc
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.
claimLet $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 in Recognition Science
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.
scope and limits
- Does not establish the remaining category axioms such as identity laws.
- Does not connect the algebraic structures to physical constants or the phi-ladder.
- Does not address morphisms that fail to preserve the golden element.
- Does not quantify over arbitrary rings outside the PhiRingObj definition.
formal statement (Lean)
556theorem phiRing_comp_assoc {A B C D : PhiRingObj}
557 (h : PhiRingHom C D) (g : PhiRingHom B C) (f : PhiRingHom A B) :
558 (phiRing_comp h (phiRing_comp g f)).map = (phiRing_comp (phiRing_comp h g) f).map := by
proof body
Term-mode proof.
559 funext x
560 rfl
561
562/-- Left identity law for `PhiRing` morphisms on underlying maps. -/