OctaveAlgObj
plain-language theorem explainer
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.
Claim. An 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
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.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.