module module high

`IndisputableMonolith.Chemistry.CrystalSymmetry`

CrystalSymmetry module enumerates the rotation orders permitted in crystallographic point groups under Recognition Science. It establishes that only orders 1, 2, 3, 4, and 6 satisfy the J-uniqueness and self-similarity conditions from the forcing chain. Condensed matter physicists would cite it when linking eight-tick periodicity to observed crystal symmetries. The module consists of definitions plus short lemmas that exclude orders 5 and 7 via upstream lattice constraints.

claimThe allowed rotation orders form the set $R = {1,2,3,4,6}$ of positive integers $n$ such that rotation by angle $2π/n$ preserves lattice structure compatible with the Recognition Composition Law and eight-tick coordination.

background

Recognition Science derives crystal symmetries from the eight-tick octave (T7) and J-function fixed point (T5). The upstream CrystalStructure module shows BCC, FCC, and HCP structures emerging from these principles, with BCC directly reflecting coordination number 8. Constants supplies the time quantum τ₀ = 1 tick. This module restricts rotations to those compatible with the phi-ladder and the RCL identity J(xy) + J(x/y) = 2J(x)J(y) + 2J(x) + 2J(y).

proof idea

This is a definition module. It defines allowedRotationOrders as the set of permitted n, then applies isCrystallographic to members of {1,2,3,4,6} while using five_not_crystallographic and seven_not_crystallographic to rule out the excluded orders via direct appeal to CrystalStructure lattice properties.

why it matters in Recognition Science

This module supplies the symmetry constraints required by the CrystalStructure module for deriving BCC, FCC, and HCP stabilities from RS principles. It closes the link from the eight-tick octave (T7) to observable crystal systems in the chemistry domain. No downstream uses are recorded yet.

scope and limits

Does not derive full point-group classifications or their character tables.
Does not address space groups or translational symmetries.
Does not compute numerical lattice parameters or binding energies.
Does not connect symmetries to specific material properties or phase transitions.

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