OctaveAlgObj
OctaveAlgObj defines objects in the octave algebra category as finite additive commutative groups equipped with an explicit additive isomorphism to ZMod 8. Algebraists assembling the Recognition Science layer system cite it when constructing LayerSysPlusObj to combine cost, phi, ledger, and octave components. The declaration is a bare structure that packages the carrier type with its AddCommGroup and Fintype instances plus the required equivalence, with no proof obligations.
claimAn object of the octave algebra category consists of a carrier type $C$ equipped with an additive commutative group structure, a finiteness structure, and an additive group isomorphism $C ≃ ℤ/8ℤ$.
background
The RecognitionCategory module builds algebraic categories for the layers of Recognition Science. OctaveAlgObj isolates the octave layer, which encodes the eight-tick periodicity (period $2^3$) from the forcing chain. The structure requires the carrier to carry an AddCommGroup instance and a Fintype instance, together with an explicit additive equivalence to ZMod 8. Morphisms are then defined separately as additive homomorphisms in the sibling OctaveAlgHom structure.
proof idea
OctaveAlgObj is a structure definition with zero proof body. It simply declares the four fields Carrier, instAddCommGroup, instFintype, and equivZModEight; the attribute declaration makes the group and finiteness instances available for type-class resolution downstream.
why it matters in Recognition Science
This definition supplies the octaveLayer field required by LayerSysPlusObj, which assembles the full calibrated system with bridge axioms (B1) and (B2). It directly realizes the eight-tick octave (T7) of the forcing chain inside the algebraic layer, with the canonical instance given by ZMod 8 itself. The construction enables the subsequent category operations octaveAlg_comp, octaveAlg_id, and their associativity and unit laws.
scope and limits
- Does not equip the carrier with any multiplicative structure.
- Does not define a cost or recognition function on the octave layer.
- Does not prove canonicity or uniqueness of the equivalence to ZMod 8.
- Does not address morphisms beyond requiring them to be additive homomorphisms.
formal statement (Lean)
669structure OctaveAlgObj where
670 Carrier : Type u
671 instAddCommGroup : AddCommGroup Carrier
672 instFintype : Fintype Carrier
673 equivZModEight : Carrier ≃+ ZMod 8
674
675attribute [instance] OctaveAlgObj.instAddCommGroup OctaveAlgObj.instFintype
676
677/-- Morphisms in `OctaveAlg` are additive homomorphisms. -/