AlgebraicStructure
plain-language theorem explainer
An inductive enumeration lists the five algebraic structures that appear when configuration dimension equals five. Certificates verifying the count of structures and the size-eight query cite this list. The definition proceeds by explicit listing of the five cases followed by automatic derivation of decidability and finiteness instances.
Claim. An inductive type is defined whose constructors are the group, the ring, the field, the module, and the vector space.
background
The module states that five canonical algebraic structures are ordered by increasing richness when the configuration dimension equals five, with each adding operations or axioms to the previous. This supplies a local variant of the inductive type defined upstream in AbstractAlgebraFromRS, whose final constructor is algebra rather than vector space. The upstream inductive type is used to establish that the cardinality equals five and to record that the third query has size eight and exponent two.
proof idea
The declaration is the inductive definition itself. Five constructors are listed explicitly and the deriving clause installs the DecidableEq, Repr, BEq, and Fintype instances with no lemmas applied.
why it matters
The enumeration populates the five_structures field inside AlgebraicStructuresCert and AbstractAlgebraCert. It supplies the concrete list required for the claim that exactly five algebraic structures exist at configuration dimension five, linking the Recognition Science forcing chain to the eight-tick octave via the size-eight abelian group.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.