isCrystallographic
plain-language theorem explainer
A natural number n is a crystallographic rotation order precisely when it belongs to the finite list {1, 2, 3, 4, 6}. Solid-state physicists cite the predicate when enumerating the 32 point groups and 7 crystal systems from space-filling constraints. The definition is a direct membership check against the precomputed allowed orders.
Claim. A natural number $n$ is crystallographic if and only if $n$ belongs to the set $1,2,3,4,6$.
background
Recognition Science derives three-dimensional space from the eight-tick octave (T7), which forces D=3. Periodic tilings of identical units in this geometry are restricted to rotation orders that permit gap-free filling, yielding the classical crystallographic restriction. The module defines the predicate directly as membership in the list of allowed orders. Upstream, allowedRotationOrders fixes the list [1, 2, 3, 4, 6] and the derivation proceeds to the 32 point groups and 7 crystal systems via combinations of these symmetries.
proof idea
The declaration is a direct definition that equates the predicate to membership in the allowed rotation orders list. Downstream theorems discharge specific cases by simp on the definition followed by decide.
why it matters
This definition supplies the predicate used to prove five-fold and seven-fold symmetries are excluded, closing the derivation of the seven crystal systems in CM-003. It implements the space-filling constraint that follows from the eight-tick structure forcing D=3 and predicts exactly five allowed rotation orders.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.