phiRing_comp
plain-language theorem explainer
The definition constructs the composite PhiRing morphism by setting its underlying map to the composition of the input maps and verifying preservation of all ring operations plus the distinguished golden element. Algebraists building the Recognition Science category would cite it when assembling layered homomorphisms such as those in LayerSysPlus. The construction proceeds by direct definition of the map field followed by six short rewrites that apply the preservation axioms of each input morphism in turn.
Claim. Let $A$, $B$, $C$ be commutative unital rings each equipped with a distinguished element satisfying the golden-ratio relation. Given structure-preserving maps $g:B→C$ and $f:A→B$ that fix zero, one, addition, negation, multiplication, and the golden element, the composite map $g∘f:A→C$ is defined by $(g∘f)(x)=g(f(x))$ and inherits all preservation properties.
background
PhiRingObj packages the algebraic data of a commutative unital ring together with a distinguished golden element and its inverse witness; the structure axioms include associativity, commutativity, and the usual ring identities. PhiRingHom consists of maps that preserve every ring operation and additionally send the golden element of the source to that of the target. The present definition supplies the missing composition operation that turns these data into a category inside the RecognitionCategory module.
proof idea
The declaration is a definition that populates a PhiRingHom record. The map field is set to ordinary function composition. Each preservation axiom is discharged by a dedicated tactic block: map_zero and map_one rewrite with the inner morphism’s axiom then apply the outer morphism’s axiom; the binary operations (add, mul) and unary operations (neg) are handled by simp using Function.comp together with the corresponding axioms of f and g; map_phi follows the same rewrite pattern as map_zero.
why it matters
The definition is invoked inside layerSysPlus_comp to assemble the PhiRing component of composite LayerSysPlus morphisms and is the direct prerequisite for the associativity theorem phiRing_comp_assoc together with the left and right identity laws phiRing_id_left and phiRing_id_right. It realizes the algebraic composition law required by the Recognition framework’s self-similar phi-structure and the eight-tick octave, closing one link in the chain from J-uniqueness to the full category of layered objects.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.