phiRing_id
plain-language theorem explainer
The identity morphism on any PhiRing object A maps the carrier to itself while preserving the ring operations and the distinguished golden element phi. Category theorists and Recognition Science algebraists cite it to confirm that PhiRing forms a category with well-behaved identities. The definition is a direct construction that sets the underlying map to the identity function and discharges the preservation axioms by reflexivity.
Claim. For any PhiRing object $A$, the identity morphism $id_A : A → A$ is the ring homomorphism whose underlying function is the identity map on the carrier of $A$; it therefore satisfies $id_A(0_A) = 0_A$, $id_A(1_A) = 1_A$, $id_A(a + b) = id_A(a) + id_A(b)$, and likewise for negation, multiplication, and the golden element $φ$.
background
PhiRingObj packages a commutative unital ring together with a distinguished element $φ$ (the golden ratio in Recognition Science units) and its inverse witness. PhiRingHom consists of functions between carriers that preserve zero, one, addition, negation, multiplication, and the golden element. The module RecognitionCategory assembles these into a category whose objects and morphisms mirror the algebraic structures appearing in the Recognition Composition Law and the phi-ladder construction. Upstream, CostAlgebra.id supplies the pattern for identity automorphisms, while ArithmeticOf.id and the Composition axiom supply the underlying preservation properties that PhiRingHom must satisfy.
proof idea
One-line wrapper that applies the identity function to the carrier and uses reflexivity to discharge the six preservation fields (map_zero through map_phi) of PhiRingHom.
why it matters
This definition supplies the identity arrows required by the PhiRing category, which are invoked directly in layerSysPlus_id to assemble the full LayerSys⁺ identity and in the left and right identity theorems phiRing_id_left and phiRing_id_right. It therefore closes the identity axioms for the algebraic layer that encodes the golden element and the Recognition Composition Law. The construction sits inside the T5–T6 segment of the forcing chain, where J-uniqueness and the self-similar fixed point phi are realized as ring data.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.