seven_not_crystallographic
plain-language theorem explainer
Seven-fold rotational symmetry cannot tile three-dimensional space periodically and is therefore excluded from crystallographic point groups. Crystallographers and condensed-matter physicists cite the result when enumerating the five allowed rotation orders that produce the 32 point groups and seven crystal systems. The proof is a one-line wrapper that unfolds the membership predicate and lets Lean decide the finite check.
Claim. $¬$ (7 is crystallographic), where a positive integer $n$ is crystallographic precisely when $n$ belongs to the list of allowed rotation orders $[1,2,3,4,6]$.
background
In the Recognition Science derivation of crystal symmetry the 8-tick octave forces three spatial dimensions. Any periodic filling of this space must respect the underlying ledger geometry, so rotational symmetries are restricted to those orders that permit gap-free tiling. The module on Crystal Symmetry Groups Derivation (CM-003) records this restriction as the crystallographic restriction theorem and lists the five permitted orders together with the resulting 32 point groups and seven crystal systems.
proof idea
The proof is a one-line wrapper. It applies simp to unfold isCrystallographic into membership in allowedRotationOrders, then invokes decide to verify that 7 lies outside the concrete list [1, 2, 3, 4, 6].
why it matters
The theorem supplies one concrete instance of the crystallographic restriction that the module uses to derive exactly five allowed rotation orders. It therefore supports the downstream claims of seven crystal systems and 32 point groups that follow from the 8-tick structure and the D = 3 constraint. No open scaffolding remains for this particular exclusion.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.