module module moderate

`IndisputableMonolith.Chemistry.CrystalSymmetry`

This module defines the allowed rotation orders and crystallographic predicates in the Recognition Science framework. Researchers modeling crystal lattices from eight-tick coordination would cite it to constrain symmetry groups. The module supplies definitions and theorems establishing exactly five permitted orders, importing the CrystalStructure and Constants modules.

claimThe allowed rotation orders form the finite set $\{1,2,3,4,6\}$ of positive integers $n$ for which a $2\pi/n$ rotation preserves lattice periodicity; the predicate isCrystallographic holds precisely on this set.

background

The upstream CrystalStructure module derives BCC, FCC, and HCP lattices from RS principles, with BCC coordination number 8 reflecting the eight-tick ledger period. Constants supplies the RS time quantum $\tau_0 = 1$ tick. The present module extends these to symmetry by introducing allowedRotationOrders together with predicates that filter rotation orders compatible with periodic boundary conditions.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

The module supplies the symmetry filter required for the CrystalSystem and numPointGroups definitions that appear among its siblings. It therefore supports the classification of crystal structures already shown to emerge from the eight-tick coordination mechanism in the CrystalStructure module.

scope and limits

Does not derive BCC, FCC, or HCP lattices.
Does not treat five-fold or seven-fold rotations beyond proving they are excluded.
Does not address non-periodic or quasicrystalline order.
Does not connect rotation orders 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