allCrystalSystems
plain-language theorem explainer
allCrystalSystems enumerates the seven crystal systems that arise under the crystallographic restriction in three dimensions. It is referenced by summation theorems that compute aggregate counts for point groups and Bravais lattices. The definition is a direct listing of the seven constructors of the CrystalSystem inductive type.
Claim. Let $C$ be the set of crystal systems. Then $C = $ {triclinic, monoclinic, orthorhombic, tetragonal, trigonal, hexagonal, cubic}.
background
The module derives crystal symmetry from the Recognition Science 8-tick structure that forces three spatial dimensions and restricts rotations to orders 1, 2, 3, 4, 6. CrystalSystem is the inductive type whose seven constructors label the distinct symmetry classes: triclinic (no essential symmetry), monoclinic (one 2-fold axis or mirror), orthorhombic (three perpendicular 2-fold axes), tetragonal (one 4-fold axis), trigonal (one 3-fold axis), hexagonal (one 6-fold axis), and cubic (four 3-fold axes along body diagonals). The module documentation states that these seven systems cluster the 32 crystallographic point groups and combine with centering types to yield 14 Bravais lattices.
proof idea
The definition is a direct enumeration that lists each constructor of the CrystalSystem inductive type.
why it matters
This definition supplies the domain for the summation theorems bravais_lattices_sum and point_groups_sum, which establish that the totals match the predicted numbers of Bravais lattices and point groups. It implements the module claim that exactly seven crystal systems emerge from the 3D space-filling rules. The list closes the enumeration step before the derivation of 14 Bravais lattices and 230 space groups.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.