module module moderate

`IndisputableMonolith.Chemistry.CrystalSymmetry`

The CrystalSymmetry module defines allowed rotation orders for crystallographic symmetries within Recognition Science. Researchers deriving BCC, FCC, and HCP structures from eight-tick coordination would cite these constraints on lattice periodicity. The module organizes definitions of rotation orders together with lemmas that exclude orders five and seven.

claimThe allowed rotation orders are the positive integers $n$ such that a rotation by angle $2\pi/n$ preserves a three-dimensional periodic lattice; the set is $\{2,3,4,6\}$.

background

This module sits in the Chemistry domain and imports CrystalStructure, whose doc states that BCC, FCC, and HCP emerge from RS principles via 8-tick coordination, and Constants, which fixes the time quantum $\tau_0 = 1$ tick. It introduces the set allowedRotationOrders, the predicate isCrystallographic, and the enumeration CrystalSystem with its counts. The upstream CrystalStructure result ties coordination number 8 directly to the 8-tick ledger period.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

The module supplies the symmetry filter required by CrystalStructure to obtain the three RS-native lattices from the eight-tick octave (T7). It feeds the classification of crystal systems and point groups that follows from the forcing chain.

scope and limits

Does not derive lattice parameters or energies.
Does not treat quasicrystals or non-periodic order.
Does not address space-group extensions beyond point groups.
Does not link to the phi-ladder or mass formula.

depends on (2)

Lean names referenced from this declaration's body.

IndisputableMonolith.Chemistry.CrystalStructure module_import
IndisputableMonolith.Constants module_import

declarations in this module (35)

def allowedRotationOrders L58
def isCrystallographic L61
theorem five_not_crystallographic L64
theorem seven_not_crystallographic L69
theorem exactly_five_rotation_orders L74
inductive CrystalSystem L79
def numCrystalSystems L90
def allCrystalSystems L93
theorem crystal_systems_count L96
def essentialSymmetry L99
def numPointGroups L111
def totalPointGroups L121
theorem point_groups_sum L123
inductive Centering L130
def numBravaisLattices L141
def totalBravaisLattices L151
theorem bravais_lattices_sum L153
def totalSpaceGroups L160
theorem space_groups_exceed_point_groups L163
structure LatticeParams L169
def validLengths L178
def triclinicConstraint L182
def monoclinicConstraint L185
def orthorhombicConstraint L189
def tetragonalConstraint L193
def cubicConstraint L197
def hexagonalConstraint L201
def trigonalConstraint L205
theorem cubic_most_constrained L211
theorem tetragonal_implies_orthorhombic L216
theorem bcc_coordination_8 L224
theorem hexagonal_fold_from_8 L227
theorem tetragonal_fold_from_8 L230
theorem trigonal_fold_from_6 L233
theorem twofold_from_8 L236