module module high

`IndisputableMonolith.Chemistry.CrystalStructure`

The CrystalStructure module introduces definitions for crystal lattices, coordination numbers, and packing efficiencies within Recognition Science. It links body-centered cubic to the eight-tick octave and shows face-centered cubic and hexagonal close-packed share packing density while body-centered cubic is lower. Materials theorists applying the phi-ladder and three-dimensional space-filling rules to solid-state properties would cite these results. The module uses direct definitions and short verification lemmas.

claimCrystal structures are defined by unit cell types, coordination numbers, and packing efficiencies, with body-centered cubic linked to the eight-tick octave and face-centered cubic sharing identical packing density with hexagonal close-packed.

background

Recognition Science derives crystal structures from periodic filling of three-dimensional space under the Unified Forcing Chain constraints, including the eight-tick octave and D=3. The module imports the fundamental time quantum τ₀ = 1 tick from Constants. It defines Structure as the geometric lattice arrangement, coordination as nearest-neighbor count, and packingEfficiency as the occupied volume fraction. Lemmas include bcc_is_8_tick connecting body-centered cubic to period 2^3, close_packed_coordination for maximum neighbors, bcc_packing_lt_fcc, and fcc_hcp_same_packing.

proof idea

This is a definition module, no proofs. It consists of type and constant definitions for structures and efficiencies, followed by lemmas that assert specific equalities and inequalities from the phi-ladder and octave constraints.

why it matters in Recognition Science

The module supplies foundational crystal structure types that feed into the Crystal Symmetry Groups Derivation (CM-003) in CrystalSymmetry. That derivation shows how the 32 crystallographic point groups and 7 crystal systems emerge from periodic unit cell constraints in 3D space under the RS mechanism.

scope and limits

Does not enumerate the 32 point groups or 7 crystal systems.
Does not derive energy scales or mass formulas for crystals.
Does not address defects, quasicrystals, or non-periodic order.
Does not compute packing efficiencies beyond the listed approximations.

used by (1)

From the project-wide theorem graph. These declarations reference this one in their body.

IndisputableMonolith.Chemistry.CrystalSymmetry module_import

depends on (1)

Lean names referenced from this declaration's body.

IndisputableMonolith.Constants module_import

declarations in this module (21)

inductive Structure L41
def coordination L48
def packingEfficiency L54
def packingEfficiencyApprox L60
theorem bcc_is_8_tick L66
theorem close_packed_coordination L69
theorem bcc_packing_lt_fcc L73
theorem fcc_hcp_same_packing L78
def idealHCPRatio L83
theorem ideal_hcp_ratio_value L86
theorem hcp_ratio_near_phi L104
def energyScale L124
theorem close_packed_lower_energy L130
def eightTickCoherence L140
theorem bcc_max_8tick_coherence L146
def stabilityScore L153
theorem stability_tradeoff L159
def prefersBCC L174
def prefersFCC L177
def prefersHCP L180
theorem alkali_prefer_bcc L183