algebraicStructure_count
plain-language theorem explainer
The theorem establishes that the inductive type enumerating five algebraic structures has cardinality exactly five. Researchers deriving algebraic structures from configuration dimension in Recognition Science would cite this to confirm the enumeration matches D = 5. The proof is a one-line decision procedure that computes the cardinality from the derived Fintype instance.
Claim. The finite type consisting of the structures group, ring, field, module, and vector space has cardinality five: $ |G| = 5 $ where $ G = $ {group, ring, field, module, vector space}.
background
The module introduces five canonical algebraic structures as an inductive type with constructors group, ring, field, moduleStruct, and vectorSpace. These are ordered by increasing richness and tied to configuration dimension D = 5. The upstream inductive type in AbstractAlgebraFromRS enumerates a similar collection with constructors group, ring, field, module, and algebra, supplying the base algebraic structures from Recognition Science.
proof idea
The proof is a one-line wrapper that applies the decide tactic to Fintype.card AlgebraicStructure = 5, using the DecidableEq, Repr, BEq, and Fintype instances derived for the inductive type.
why it matters
This cardinality result supplies the five_structures field in the downstream algebraicStructuresCert definition. It completes the enumeration step for algebraic structures derived from configDim in the Recognition Science framework, where the count of five aligns with D = 5. The result touches no open questions since the proof is complete and contains no sorry.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.