crystal_systems_count
plain-language theorem explainer
The declaration confirms that the explicitly enumerated list of crystal systems contains precisely seven entries, aligning with the count required by the Recognition Science derivation of crystallographic symmetry. Researchers modeling crystal structures under the RS framework would cite this to validate the enumeration of the seven systems: triclinic through cubic. The proof is a direct reflexivity step that equates the list length to the constant seven by definition.
Claim. The length of the list enumerating all crystal systems equals seven: $|$ {triclinic, monoclinic, orthorhombic, tetragonal, trigonal, hexagonal, cubic} $| = 7$.
background
In the Crystal Symmetry module, crystal systems arise from the constraints of periodic filling of 3D space, which itself follows from the eight-tick structure in the foundational RS forcing chain. The definition allCrystalSystems constructs the explicit list of the seven systems, while numCrystalSystems is the natural number seven. This local setting builds on the space-filling restrictions that prohibit five-fold and seven-fold rotations, as detailed in the module documentation.
proof idea
The proof is a one-line wrapper applying reflexivity (rfl) to the definitional equality between the length of the allCrystalSystems list and the constant numCrystalSystems.
why it matters
This theorem anchors the count of exactly seven crystal systems within the RS framework, as predicted by the module's derivation from the 8-tick octave and 3D space constraints. It supports the clustering of the 32 point groups into these seven systems, consistent with the predictions of exactly seven crystal systems and fourteen Bravais lattices. No open questions are directly addressed here, but it closes the enumeration step in the symmetry derivation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.