octaveAlg_comp_assoc
plain-language theorem explainer
Associativity holds for composition of morphisms in the OctaveAlg category, where objects are additive groups isomorphic to ZMod 8 and morphisms are additive homomorphisms. Algebraists verifying category axioms for the eight-tick structure in Recognition Science would cite this to confirm composition behaves as expected. The proof is a one-line term wrapper applying extensionality to the underlying maps followed by reflexivity.
Claim. For objects $A,B,C,D$ each an additive group isomorphic to $Z/8Z$, and morphisms $h:C→D$, $g:B→C$, $f:A→B$ given by additive homomorphisms, the underlying maps satisfy $(h∘(g∘f))=( (h∘g)∘f )$.
background
Objects in OctaveAlg are additive commutative groups with a Fintype instance and an explicit isomorphism to ZMod 8, encoding the eight-tick octave period. Morphisms are additive group homomorphisms between the carriers. The upstream definition octaveAlg_comp constructs the composite morphism by composing the underlying maps via g.map.comp f.map.
proof idea
The term-mode proof applies the ext tactic to obtain function extensionality on the maps, then concludes by reflexivity. Associativity follows directly because map composition is defined via the standard composition of additive homomorphisms, which is associative in the ambient type theory.
why it matters
This theorem supplies the associativity axiom for the OctaveAlg category, realizing the T7 eight-tick octave algebraically within the Recognition framework. It parallels recAlg_comp_assoc in the same module and supports higher constructions involving cost families and recognition objects. No downstream uses are recorded yet.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.