space_groups_exceed_point_groups
plain-language theorem explainer
The declaration shows that the total count of crystallographic space groups exceeds the count of point groups. Solid-state physicists and crystallographers cite this when distinguishing the 230 space groups from the 32 point groups in periodic 3D structures. The proof reduces to a direct numerical comparison that evaluates true by computation.
Claim. The number of crystallographic space groups exceeds the number of crystallographic point groups: $230 > 32$.
background
In the Crystal Symmetry module, totalPointGroups is defined as 32 and totalSpaceGroups as 230. The module derives these counts from the 8-tick structure that forces three spatial dimensions, restricting rotations to orders 1, 2, 3, 4, and 6 so that identical units tile space periodically. Space groups extend point groups by adding translations such as screws and glides. The upstream definition totalPointGroups records the 32 crystallographic point groups obtained by combining allowed rotations, reflections, and inversions. The upstream definition totalSpaceGroups records the 230 groups that result once translations are included.
proof idea
The term proof applies native_decide directly to the inequality between the two constant definitions. No further lemmas or tactics are invoked; the decision procedure confirms 230 exceeds 32 by arithmetic evaluation.
why it matters
This result confirms the module prediction that exactly 230 space groups arise once translations augment the 32 point groups. It supports the RS claim that the eight-tick octave forces three dimensions and that space-filling constraints limit rotations to five orders. The declaration closes the enumeration step in the crystal symmetry derivation and aligns with the downstream count of 230 groups that appears in the module's summary of Bravais lattices and space-group totals.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.