exactly_five_rotation_orders
plain-language theorem explainer
The crystallographic restriction asserts that periodic tiling of three-dimensional space admits only five rotation orders. Solid-state physicists and crystallographers cite the result when counting the 32 point groups and seven crystal systems that follow from the eight-tick ledger geometry. The proof is a direct reflexivity reduction against the explicit list definition of allowed rotation orders.
Claim. The set of rotation orders compatible with periodic filling of three-dimensional Euclidean space has cardinality five: $1,2,3,4,6$.
background
The module derives crystal symmetry from the Recognition Science eight-tick structure, which forces three spatial dimensions, and from the requirement that identical unit cells tile space without gaps. A rotation order is crystallographic precisely when it permits such periodic tiling. The upstream definition supplies the explicit list of allowed orders as the natural numbers 1, 2, 3, 4 and 6.
proof idea
One-line wrapper that applies reflexivity to the length of the explicit list definition of allowed rotation orders.
why it matters
The declaration records the first explicit prediction listed in the module doc-comment: only five allowed rotation orders. It supplies the numerical foundation for the subsequent clustering into seven crystal systems and thirty-two point groups. The result is tied directly to the eight-tick octave and the three-dimensional constraint derived earlier in the framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.