totalSpaceGroups
plain-language theorem explainer
Recognition Science predicts exactly 230 crystallographic space groups once translations are added to the 32 point groups in three dimensions. Condensed-matter physicists cite the constant when verifying that screw and glide operations enlarge the symmetry count beyond the point-group total. The declaration is a direct numerical assignment with no lemmas or tactics.
Claim. The total number of crystallographic space groups is $230$.
background
Crystal symmetry emerges from the eight-tick octave that forces three spatial dimensions. Periodic filling of this space restricts rotations to orders 1, 2, 3, 4, and 6, producing 32 point groups that cluster into 7 crystal systems and 14 Bravais lattices. The module states that including translations yields exactly 230 space groups.
proof idea
The declaration is a direct definition that assigns the integer 230. No lemmas are applied and no tactics are used; the value is asserted to match the standard crystallographic enumeration consistent with the space-filling constraint.
why it matters
This constant completes the crystal-symmetry chain from the eight-tick octave and D=3 to the full space-group count. It is referenced by the theorem space_groups_exceed_point_groups, which shows translations increase the total beyond the point-group count. The module documentation states that the RS mechanism predicts exactly 230 space groups when including translations.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.