AlgebraicStructuresCert
plain-language theorem explainer
AlgebraicStructuresCert packages the assertion that exactly five algebraic structures exist at configuration dimension five. Researchers tracing the Recognition Science derivation of algebra from configDim would cite it to anchor the hierarchy count. The declaration is a bare structure definition whose single field directly encodes the Fintype cardinality condition.
Claim. The structure Cert requires that the finite set of algebraic structures has cardinality five, where the enumerated structures are the group, the ring, the field, the module, and the vector space.
background
The module defines five canonical algebraic structures ordered by increasing richness at configDim D = 5: group, ring, field, module, and vector space, each adding operations or axioms to the previous. The referenced inductive type AlgebraicStructure enumerates precisely these five constructors and derives Fintype. The upstream inductive in AbstractAlgebraFromRS lists a similar collection that replaces the last two entries with an algebra variant.
proof idea
The declaration is a structure definition containing one field. The field states the cardinality equality using the Fintype instance already derived on the inductive type; no tactics or lemmas are applied.
why it matters
This supplies the type for the downstream certificate algebraicStructuresCert that records the count five. It completes the local step that matches algebraic richness to configDim = 5 inside the mathematics module. The construction supports the broader claim that the Recognition framework produces exactly five levels of algebraic structure when the configuration dimension reaches five.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.