Chemistry Crystal Symmetry Seven Not Crystallographic

The sevenfold exclusion

The crystallographic restriction theorem is a classical result: in a crystal, a periodic arrangement of atoms filling space, the only rotational symmetries possible are 1-fold, 2-fold, 3-fold, 4-fold, and 6-fold. A 5-fold or 7-fold rotation would force the pattern to overlap or leave gaps, so it cannot tile space periodically. This is why snowflakes show sixfold symmetry and no natural crystal shows fivefold or sevenfold symmetry in its atomic lattice.

In the Recognition Science framework, this restriction appears as a formal statement in a machine-checked library of theorems. The declaration seven_not_crystallographic states that 7 is not a crystallographic rotation order. The proof is a direct computation: the library defines the allowed rotation orders as the list [1, 2, 3, 4, 6], defines a rotation order as crystallographic if it appears in that list, and then checks that 7 does not. The companion declaration five_not_crystallographic does the same for 5.

The framework's account derives these restrictions from a deeper structure. It models three-dimensional space as arising from an eight-tick recognition cycle, a discrete record of events that forces the geometry of the lattice. The library then proves that the allowed rotation orders follow from this structure, and it records the classical consequences: exactly 32 crystallographic point groups, 7 crystal systems, 14 Bravais lattices, and 230 space groups. These counts match the standard results of crystallography.

What the declaration does not claim is that 7-fold symmetry is impossible in all contexts. Quasicrystals, discovered by Dan Shechtman in 1982, show 5-fold and 10-fold symmetry in a non-periodic arrangement. The theorem concerns periodic space-filling lattices only. It also does not claim that the framework's derivation of three-dimensional space from the eight-tick cycle is a proved theorem; that bridge remains open. The exclusion of 7-fold rotation is a proved fact about the defined list, not a claim about every possible physical structure.

/-- 7-fold symmetry is NOT crystallographic. -/
theorem seven_not_crystallographic : ¬isCrystallographic 7 := by
  simp only [isCrystallographic, allowedRotationOrders]
  decide

/-- The allowed rotation orders in crystallography. -/
def allowedRotationOrders : List ℕ := [1, 2, 3, 4, 6]

/-- Total number of crystallographic point groups. -/
def totalPointGroups : ℕ := 32

/-- Number of crystal systems. -/
def numCrystalSystems : ℕ := 7

/-- Total number of Bravais lattices. -/
def totalBravaisLattices : ℕ := 14

/-- Total number of crystallographic space groups. -/
def totalSpaceGroups : ℕ := 230

/-- There are exactly 5 allowed rotation orders. -/
theorem exactly_five_rotation_orders : allowedRotationOrders.length = 5 := by rfl

What this page does not claim

The declaration does not claim that 5-fold or 7-fold symmetry is impossible in non-periodic structures such as quasicrystals. The declaration does not claim that the framework's derivation of three-dimensional space from the eight-tick cycle is a proved theorem. The declaration does not claim that the framework's model of crystal symmetry is the only way to derive the crystallographic restriction.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/Chemistry/CrystalSymmetry.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red: