packingEfficiency
plain-language theorem explainer
Packing efficiency assigns to each crystal structure the volume fraction occupied by hard spheres in the lattice. Researchers comparing metallic lattice stabilities cite these values when ordering cohesive energies under Recognition Science. The definition performs direct case analysis on the three constructors of the Structure type and returns the classical geometric expressions.
Claim. Let $S$ be a crystal structure. The packing efficiency is defined as $frac{pi sqrt{3}}{8}$ for body-centered cubic and $frac{pi}{3 sqrt{2}}$ for both face-centered cubic and hexagonal close-packed.
background
The Structure inductive classifies crystals into body-centered cubic, face-centered cubic, and hexagonal close-packed. The module states that these structures emerge from Recognition Science principles: BCC coordination reflects the eight-tick ledger period while FCC and HCP achieve maximum packing with coordination 12. Packing efficiency is the fraction of space filled by spheres and relates to cohesive energy ordering with FCC approximately equal to HCP and both exceeding BCC.
proof idea
The definition is a direct pattern match on the Structure inductive type. Each case returns the standard closed-form expression involving pi and square roots with no further lemmas or computation.
why it matters
This supplies the exact packing fractions used to prove FCC and HCP denser than BCC in the downstream theorem fcc_hcp_denser_than_bcc. It implements the energy-ordering prediction from the crystal-structure stability analysis and connects to the eight-tick coordination for BCC together with close-packing for FCC and HCP.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.