AlgebraicStructure
The inductive type enumerating algebraic structures for configuration dimension 5 lists group, ring, field, module and vector space in order of increasing richness. A researcher counting or certifying these structures within the Recognition Science algebra module would cite this definition. It is introduced as a plain inductive type with derived instances for decidable equality and finiteness.
claimThe algebraic structures form the inductive type generated by the five constructors group, ring, field, module and vector space.
background
The module documentation fixes configDim at 5 to produce exactly these five structures ordered by increasing algebraic richness. The upstream AlgebraicStructure inductive type from AbstractAlgebraFromRS enumerates group, ring, field, module and algebra; the present variant substitutes moduleStruct and vectorSpace to match the configDim convention.
proof idea
The declaration is a direct inductive definition that introduces five constructors and derives the DecidableEq, Repr, BEq and Fintype instances.
why it matters in Recognition Science
It supplies the type used by AlgebraicStructuresCert to assert cardinality 5 and by algebraicStructure_count to compute that cardinality by decision. The definition enumerates the algebraic hierarchy tied to configDim = 5, consistent with the Recognition framework derivation of structures from the forcing chain.
scope and limits
- Does not specify operations or axioms for any listed structure.
- Does not derive theorems about homomorphisms or representations.
- Does not connect the structures to J-cost, defectDist or the phi-ladder.
- Does not address extensions or variants beyond configDim = 5.
formal statement (Lean)
18inductive AlgebraicStructure where
19 | group
20 | ring
21 | field
22 | moduleStruct
23 | vectorSpace
24 deriving DecidableEq, Repr, BEq, Fintype
25