PhiRingHom
PhiRingHom defines morphisms between PhiRing objects that preserve the full ring operations plus the distinguished golden element phi. Algebraists constructing the Recognition Science category layer cite this when building composition and identity laws for phi-ring data. The declaration is a bare structure with no proof body or attached lemmas.
claimA morphism from PhiRing object $A$ to $B$ is a map $f: A.Carrier → 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 with zero, one, add, neg, mul, plus associativity and commutativity axioms) together with a distinguished element phi and its inverse witness. The RecognitionCategory module uses this to model the algebraic core of Recognition Science, where phi is the self-similar fixed point forced by the T5–T6 steps of the unified forcing chain. Upstream results supply the underlying arithmetic: mul and neg are lifted from IntegersFromLogic and ArithmeticFromLogic, while the elliptic-curve neg is imported only for auxiliary use.
proof idea
This is a structure definition; the fields directly list the required preservation properties with no lemmas, tactics, or reduction steps applied.
why it matters in Recognition Science
PhiRingHom supplies the morphism data for the PhiRing category, which is required by LayerSysPlusHom and by the composition and identity theorems phiRing_comp, phiRing_id, phiRing_id_left, and phiRing_id_right. It encodes the algebraic layer that supports the phi-ladder, the eight-tick octave, and the Recognition Composition Law through preserved multiplication. The definition closes the basic categorical scaffolding for the paper-facing algebra before higher layer-system constructions are assembled.
scope and limits
- Does not assert existence of non-identity morphisms between arbitrary objects.
- Does not impose continuity, topology, or metric structure on the carrier.
- Does not reference J-cost, defectDist, or the phi-ladder mass formula.
- Does not address associators or higher categorical coherence beyond basic composition.
formal statement (Lean)
485structure PhiRingHom (A B : PhiRingObj) where
486 map : A.Carrier → B.Carrier
487 map_zero : map A.zero = B.zero
488 map_one : map A.one = B.one
489 map_add : ∀ a b, map (A.add a b) = B.add (map a) (map b)
490 map_neg : ∀ a, map (A.neg a) = B.neg (map a)
491 map_mul : ∀ a b, map (A.mul a b) = B.mul (map a) (map b)
492 map_phi : map A.phi = B.phi
493
494/-- Identity morphism in `PhiRing`. -/