PhiRingHom
plain-language theorem explainer
PhiRingHom defines morphisms between PhiRingObj carriers that preserve the full ring operations together with the distinguished golden element. Category theorists and Recognition Science algebraists cite it when assembling LayerSysPlusHom or verifying composition and identity laws for the phi component. The declaration is a direct structure bundling the six preservation axioms with no additional lemmas or tactics.
Claim. A morphism $f : A.to B$ between PhiRing objects is a map $f : A.Carrier to B.Carrier$ satisfying $f(0_A)=0_B$, $f(1_A)=1_B$, $f(a +_A b)=f(a)+_B f(b)$, $f(-_A a)=- _B f(a)$, $f(a ·_A b)=f(a)·_B f(b)$, and $f(φ_A)=φ_B$.
background
PhiRingObj packages a commutative unital ring (Carrier, zero, one, add, neg, mul) together with a distinguished element phi. The RecognitionCategory module builds four parallel algebraic layers (cost, phi-ring, ledger, octave) whose morphisms are later combined in LayerSysPlusHom. Upstream, PhiRingObj supplies the objects; basic ring operations are imported from ArithmeticFromLogic and IntegersFromLogic.
proof idea
One-line structure definition that directly records the six preservation conditions. No lemmas are invoked and no tactics appear; the fields are the axioms themselves.
why it matters
Supplies the phi-layer morphism type used by LayerSysPlusHom and by the composition and identity theorems phiRing_comp, phiRing_id, phiRing_id_left, phiRing_id_right. It ensures that maps in the Recognition framework respect the self-similar fixed point phi (T6) and the ring structure derived from the forcing chain. The declaration closes the morphism interface for the phi component before the full LayerSysPlus category is assembled.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.