OctaveAlgHom
OctaveAlgHom defines morphisms in the octave algebra category as additive group homomorphisms between carriers of objects equivalent to Z/8Z. Layered category constructions in Recognition Science cite this when assembling morphisms for the full system. The definition is a direct structure that encodes only the additive homomorphism requirement on the carriers.
claimLet $A$ and $B$ be octave algebra objects, each with carrier an additive commutative group isomorphic to $Z/8Z$. A morphism from $A$ to $B$ consists of an additive group homomorphism $map : A.Carrier → B.Carrier$.
background
The RecognitionCategory module equips each layer of the Recognition Science framework with its own algebraic category. The octave layer encodes the discrete eight-tick periodicity that appears as the fundamental evolution period in Constants.octave (one octave equals 8 ticks) and MusicalScale.octave (ratio 2). Upstream, ArithmeticOf.canonical supplies the initial arithmetic object whose realization independence is preserved here, while IntegrationGap.A fixes the active edge count per tick at 1.
proof idea
This is a structure definition whose single field map is typed as an AddMonoidHom between the carriers of the two OctaveAlgObj arguments. No lemmas or tactics are invoked; the declaration itself supplies the morphism data.
why it matters in Recognition Science
OctaveAlgHom supplies the morphism component for the octave layer inside LayerSysPlusHom, which packages cost, phi, ledger, and octave homomorphisms together. It directly enables the downstream definitions octaveAlg_comp, octaveAlg_id and the identity and associativity theorems that verify the category axioms. In the framework this realizes the eight-tick octave (T7) as an algebraic object, feeding the Recognition Composition Law and the derivation of three spatial dimensions.
scope and limits
- Does not require homomorphisms to preserve the explicit ZMod 8 equivalence.
- Does not equip morphisms with continuity, metrics, or ring structure.
- Does not define composition or identities; those appear in separate declarations.
- Does not link directly to J-cost, defect distance, or the phi-ladder.
formal statement (Lean)
678structure OctaveAlgHom (A B : OctaveAlgObj) where
679 map : A.Carrier →+ B.Carrier
680
681/-- The canonical octave object represented by `ZMod 8`. -/