canonicalOctaveAlgObj
plain-language theorem explainer
This definition supplies the standard object in the OctaveAlg category as the cyclic group of order 8. Researchers assembling the full layered system in Recognition Science cite it when combining cost, phi, ledger, and octave components. The construction is a direct structure instance on ZMod 8 that pulls the required group and finiteness instances automatically and uses the reflexive additive equivalence.
Claim. The canonical object of the octave algebra category is the additive group $Z/8Z$ equipped with its standard additive commutative group structure, finite type structure, and the identity additive isomorphism to itself.
background
The RecognitionCategory module organizes algebraic carriers that realize the layers of Recognition Science. OctaveAlgObj is the structure whose objects are additive commutative groups that are finite and equipped with an explicit additive equivalence to the standard $ZMod 8$. This encodes the eight-tick octave (T7) of the forcing chain, whose period is $2^3$ and which supplies the discrete time structure used downstream.
proof idea
One-line wrapper that constructs an OctaveAlgObj by setting the carrier to ZMod 8, obtaining the AddCommGroup and Fintype instances via inferInstance, and supplying the reflexive additive equivalence AddEquiv.refl _.
why it matters
It provides the octave layer inside canonicalLayerSysPlus, the canonical linked system that assembles verified cost algebra, phi ring, ledger algebra, and octave algebra. This realizes the T7 eight-tick octave step of the forcing chain and supplies the concrete model required for any higher derivation that needs the discrete octave structure. No open question is closed; the definition simply fixes the standard representative.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.