octaveAlg_id_right
plain-language theorem explainer
The right identity law for OctaveAlg morphisms states that composing any additive homomorphism f on the right with the identity on its domain leaves the underlying map unchanged. Algebraists checking the categorical axioms of the eight-tick octave layer would cite this when assembling the Recognition Category. The proof is a term-mode one-liner that reduces via function extensionality and concludes by reflexivity after unfolding composition and identity.
Claim. Let $A,B$ be objects of the octave algebra (additive groups isomorphic to $Z/8Z$). For any morphism $f:A→B$ given by an additive homomorphism, the composition of $f$ with the identity on $A$ satisfies $(f∘id_A).map=f.map$.
background
The RecognitionCategory module assembles the octave algebra layer on top of CostAlgebra and PhiRing to encode the eight-tick structure. OctaveAlgObj packages an additive commutative group that is finite and equipped with an explicit isomorphism to ZMod 8. OctaveAlgHom consists solely of the additive homomorphisms between such carriers. Composition is defined by ordinary map composition, while the identity supplies the standard AddMonoidHom.id. This layer sits inside the larger Recognition Category whose morphisms must obey the Recognition Composition Law.
proof idea
The term proof applies function extensionality to the underlying maps, then reflexivity. It relies on the definitions of octaveAlg_comp (which composes the maps) and octaveAlg_id (which supplies the identity map) to obtain definitional equality after the ext step.
why it matters
The result supplies the right unit law required for OctaveAlg to be a category, parallel to the sibling recAlg_id_right in the Recognition Algebra layer. It anchors the T7 eight-tick octave inside the forcing chain by confirming that identity morphisms act as units under composition. No downstream theorems are recorded yet, but the law is a prerequisite for any further embedding of the octave structure into mass formulas or the phi-ladder.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.