phiRing_id_left
In the PhiRing category, for any morphism f from A to B the composition of the identity on B with f recovers the underlying map of f exactly. Researchers formalizing algebraic layers of Recognition Science or verifying that PhiRing forms a category would cite this when checking identity axioms. The proof is a one-line wrapper that applies function extensionality to the map component and then reflexivity.
claimLet $A$ and $B$ be commutative unital rings each equipped with a distinguished golden element. For any ring homomorphism $f: A to B$ that also sends the golden element of $A$ to that of $B$, the composition of the identity morphism on $B$ with $f$ has the same underlying function as $f$.
background
PhiRingObj consists of a carrier type together with zero, one, addition, negation and multiplication satisfying the commutative unital ring axioms, plus a distinguished golden element. PhiRingHom consists of functions between carriers that preserve zero, one, addition, negation, multiplication and the golden element. Composition of two such morphisms is defined by composing their underlying functions, while the identity morphism on an object is the identity function on its carrier. This declaration lives in the RecognitionCategory module, which assembles categorical data for algebraic objects appearing in the Recognition Science framework and imports CostAlgebra, PhiRing, LedgerAlgebra and OctaveAlgebra.
proof idea
One-line wrapper that applies function extensionality to the underlying map of the composite morphism and then reflexivity. The composite map is literally the original map by the definition of phiRing_comp applied to phiRing_id.
why it matters in Recognition Science
It supplies the left identity axiom for the PhiRing category, a prerequisite for treating morphisms as composable arrows in the algebraic layer of Recognition Science. The result sits alongside the sibling recAlg_id_left and supports the larger program of embedding J-cost structures and the phi-ladder into categorical language. No downstream uses are recorded yet, but the declaration closes one of the standard category axioms required before any further composition or universal-property arguments can be stated.
scope and limits
- Does not establish the right identity law for PhiRing morphisms.
- Does not prove associativity of composition.
- Does not address any physical interpretation such as mass ladders or constants.
- Does not treat non-commutative or non-unital variants of the ring data.
- Does not connect the identity law to the Recognition Composition Law or forcing chain steps.
formal statement (Lean)
563theorem phiRing_id_left {A B : PhiRingObj} (f : PhiRingHom A B) :
564 (phiRing_comp (phiRing_id B) f).map = f.map := by
proof body
Term-mode proof.
565 funext x
566 rfl
567
568/-- Right identity law for `PhiRing` morphisms on underlying maps. -/