Chemistry Crystal Symmetry Five Not Crystallographic

The crystallographic restriction

The crystallographic restriction is a classical result of solid state physics: in a periodic crystal, the only rotational symmetries that can appear are 1-, 2-, 3-, 4-, and 6-fold. A 5-fold rotation, which turns a pattern by 72 degrees, cannot occur in a periodic tiling of three-dimensional space. The same holds for any rotation of order 7 or higher. The proof is geometric: fivefold symmetry is incompatible with the requirement that identical unit cells fill space without gaps or overlaps.

The standard derivation starts from the observation that a lattice is a discrete set of points with translational symmetry. If a lattice has a rotation of order n, then the distance between two lattice points must be preserved by that rotation. Applying the rotation to a nearest-neighbor vector and subtracting the original vector gives a new lattice vector whose length is 2 cos(360°/n) times the original. Since this new vector cannot be shorter than the nearest-neighbor distance, one obtains |2 cos(360°/n)| ≥ 1, which restricts n to 1, 2, 3, 4, or 6. The case n = 5 fails because 2 cos(72°) ≈ 0.618, which is less than 1.

This restriction is the foundation of the classification of crystal symmetry. It leads to exactly 32 crystallographic point groups, which cluster into 7 crystal systems, and combining these with centering options gives 14 Bravais lattices. Including translations yields 230 space groups. These numbers are standard results of crystallography, taught in every solid state physics course.

In Recognition Science, the framework models the same restriction through its own derivation. The framework's machine-checked library of formal theorems contains a declaration named five_not_crystallographic, which states that the integer 5 is not a crystallographic rotation order. This is a formal theorem: it is proved by checking the definition of crystallographic order against the allowed list [1, 2, 3, 4, 6]. The library also proves the analogous statement for 7. These are not new physical predictions; they are formal restatements of the classical crystallographic restriction within the framework's own language.

The framework's contribution is not the restriction itself, which is classical, but the claim that the eight-tick structure of its recognition cycle forces three spatial dimensions, and that this three-dimensionality then imposes the same restriction on periodic arrangements. The library's declarations for the seven crystal systems and their constraints (for example, the cubic constraint that all lengths are equal and all angles are 90 degrees) are definitions, not derivations from deeper principles. What the framework proves is the internal consistency of its model: given its definitions, the fivefold rotation is indeed excluded.

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

/-- 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

What this page does not claim

The framework does not prove that real crystals obey this restriction; that is an empirical fact of solid state physics. The declaration five_not_crystallographic does not derive the restriction from the recognition ledger; it merely checks membership in a defined list. The framework does not claim to predict the existence of quasicrystals, which exhibit fivefold symmetry without periodic order.

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: