numPointGroups
plain-language theorem explainer
numPointGroups assigns integer counts of crystallographic point groups to each of the seven crystal systems: 2 for triclinic, 3 for monoclinic and orthorhombic, 7 for tetragonal and hexagonal, 5 for trigonal and cubic. A solid-state physicist or crystallographer cites the map when confirming that these systems partition the 32 groups allowed by periodic filling of three-dimensional space. The definition is an exhaustive case split on the CrystalSystem inductive type.
Claim. Let $C$ be the set of crystal systems with elements triclinic, monoclinic, orthorhombic, tetragonal, trigonal, hexagonal, cubic. The function $n: C → ℕ$ is defined by $n$(triclinic)$=2$, $n$(monoclinic)$=3$, $n$(orthorhombic)$=3$, $n$(tetragonal)$=7$, $n$(trigonal)$=5$, $n$(hexagonal)$=7$, $n$(cubic)$=5$.
background
The module shows crystal symmetry arising from the 8-tick structure that forces three spatial dimensions. Periodic unit-cell arrangements in 3D restrict rotations to orders 1, 2, 3, 4, 6; 5-fold and higher symmetries cannot tile space without gaps. The seven crystal systems then classify the resulting 32 point groups by their essential symmetry elements: triclinic has none, 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.
proof idea
The definition is a direct pattern match on the seven constructors of the CrystalSystem inductive type, returning the tabulated integer for each case. No lemmas or tactics are invoked; it is a pure data definition.
why it matters
The definition supplies the per-system counts that the downstream theorem point_groups_sum sums to totalPointGroups (32). It completes the enumeration step in the CM-003 derivation, which traces the seven systems and 32 groups to the 8-tick octave and D=3 constraint. The module states that exactly 32 crystallographic point groups and exactly 7 crystal systems follow from space-filling in three dimensions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.