allowedRotationOrders
plain-language theorem explainer
The definition supplies the five rotation orders permitted for periodic lattices in three dimensions. Researchers deriving the seven crystal systems or the 32 point groups cite this list when applying space-filling constraints. It is supplied directly as a constant list with no computation or lemmas.
Claim. The allowed rotation orders for crystallographic symmetries in three-dimensional space are the positive integers $1, 2, 3, 4, 6$.
background
Crystal symmetry groups arise from the requirement that identical unit cells fill three-dimensional space periodically. The module derives this from the eight-tick structure that forces three spatial dimensions, which restricts rotations to those compatible with the underlying ledger geometry. Upstream results on active edge counts per tick and simplicial edge lengths supply the coherence constraints that enforce the space-filling rule.
proof idea
The declaration is a direct definition that introduces the constant list of five orders. No lemmas or tactics are invoked; it functions as the base datum for sibling definitions and theorems.
why it matters
This definition feeds the theorems that establish exactly five allowed orders and exclude five-fold and seven-fold symmetries. It realizes the module prediction that only these orders satisfy the space-filling constraint derived from the eight-tick octave and D equals three. It anchors the derivation of the seven crystal systems and 32 point groups within the Recognition framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.