octaveAlg_comp
plain-language theorem explainer
Composition of morphisms in the OctaveAlg category is defined by composing the underlying additive maps of the homomorphisms. Researchers assembling the layered algebraic structures in Recognition Science cite this definition when constructing composite morphisms across the octave component. The definition is a one-line wrapper that delegates directly to the standard composition of additive group homomorphisms between carriers isomorphic to Z/8Z.
Claim. Given objects $A, B, C$ in the octave algebra category (each an additive group isomorphic to $Z/8Z$), and morphisms $g: B → C$, $f: A → B$ that are additive homomorphisms, the composite morphism $A → C$ is the additive homomorphism whose carrier map is the composition $g ∘ f$.
background
Objects in the OctaveAlg category are additive commutative groups equipped with an explicit isomorphism to the cyclic group of order 8. Morphisms are additive homomorphisms between the carriers of these objects. This category encodes the eight-tick octave structure arising in the Recognition Science forcing chain at step T7.
proof idea
This is a one-line definition. It constructs the resulting OctaveAlgHom by setting its map field to the composition of the input maps g.map and f.map, reusing the standard composition operation on additive group homomorphisms.
why it matters
This definition supplies the octave morphism composition required by layerSysPlus_comp, which assembles the full LayerSys⁺ structure from cost, phi-ring, ledger, and octave layers. It enables the downstream theorems on associativity, left identity, and right identity for OctaveAlg morphisms. In the framework it closes the algebraic operations needed for the Recognition Composition Law and discrete phi-ladder constructions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.