CrystalSystem
plain-language theorem explainer
CrystalSystem enumerates the seven crystal systems that arise when periodic unit cells fill three-dimensional space under the eight-tick ledger constraint. Crystallographers and materials theorists cite the enumeration when mapping essential symmetries to point-group counts and Bravais lattices inside the Recognition Science derivation. The declaration is a direct inductive type whose seven constructors match the standard classification with no additional proof obligations.
Claim. CrystalSystem is the inductive type whose constructors are triclinic, monoclinic, orthorhombic, tetragonal, trigonal, hexagonal, and cubic.
background
The module derives crystal symmetry from the Recognition Science mechanism in which the eight-tick structure forces three spatial dimensions. Any periodic filling of that space restricts rotations to orders 1, 2, 3, 4, and 6; five-fold and higher symmetries cannot tile without gaps. The seven systems then cluster the resulting 32 point groups by their essential symmetry elements: none for triclinic, one 2-fold axis for monoclinic, three perpendicular 2-fold axes for orthorhombic, one 4-fold for tetragonal, one 3-fold for trigonal, one 6-fold for hexagonal, and four 3-fold body diagonals for cubic.
proof idea
The declaration is an inductive definition that directly lists the seven constructors. No upstream lemmas are invoked; the type is introduced to serve as the domain for the sibling functions allCrystalSystems, essentialSymmetry, numPointGroups, and numBravaisLattices.
why it matters
The definition supplies the enumeration required by allCrystalSystems, essentialSymmetry, numPointGroups, and numBravaisLattices to recover the predicted counts of 32 point groups and 14 Bravais lattices. It realizes the module-level claim that the eight-tick forcing of three dimensions plus the crystallographic restriction yields exactly seven systems. The construction therefore bridges the ledger geometry of PhiForcingDerived and SpectralEmergence to concrete crystal classification.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.