AlgebraicStructure
plain-language theorem explainer
The AlgebraicStructure inductive type enumerates the five algebraic structures that arise from the recognition lattice Q₃. Researchers tracing algebraic consequences of Recognition Science cite this enumeration when confirming that configDim D equals 5. The definition proceeds by direct inductive listing of the five constructors together with automatic derivation of decidable equality and finiteness.
Claim. Let $A$ be the inductive type whose constructors are the group, the ring, the field, the module, and the algebra. Then the cardinality of $A$ equals 5.
background
The recognition lattice Q₃ is realized as the abelian group (ℤ/2)³ of order 8, which equals 2^D for D = 3 spatial dimensions forced by the UnifiedForcingChain. The module states that this lattice carries a natural algebraic structure whose canonical forms are exactly five in number. An upstream inductive definition in AlgebraicStructuresFromConfigDim supplies a parallel enumeration whose constructors are group, ring, field, moduleStruct, and vectorSpace.
proof idea
The declaration is a direct inductive definition. Lean supplies the deriving clauses for DecidableEq, Repr, BEq, and Fintype with no separate proof body or tactic steps required.
why it matters
This definition supplies the type whose cardinality is asserted to be 5 in the downstream theorem algebraicStructureCount and in the certificate AbstractAlgebraCert. It realizes the claim that Q₃ supports exactly five algebraic structures when D = 3, linking directly to the eight-tick octave (period 2^3) and the dimension D = 3. The construction closes one step in the algebraic consequences of the Recognition Composition Law.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.