packingEfficiency
plain-language theorem explainer
The definition assigns packing efficiencies to metallic lattice types as 0.68 for BCC and 0.74 for both FCC and HCP. Researchers comparing crystal densities in metallic bonding models cite these values when invoking 8-tick coherence and coordination numbers. It is realized by direct case analysis on the three constructors of LatticeType.
Claim. Define the packing efficiency function $η$ on lattice types by $η( BCC ) = 0.68$, $η( FCC ) = 0.74$, $η( HCP ) = 0.74$.
background
The MetallicBond module derives metallic bonding from valence electron delocalization that minimizes recognition cost across a lattice, with the metallic state forming a coherent many-body system under an 8-tick rhythm. LatticeType is the inductive classification of structures by coordination number: BCC at 8 and FCC/HCP at 12. Packing efficiency is the conventional fraction of space filled by spheres in each lattice. Upstream CrystalStructure supplies the exact geometric expressions (for example $π √3 / 8$ for BCC) together with the coordination definition; Constants.tick fixes the fundamental time quantum.
proof idea
Direct definition by cases on the LatticeType inductive type, returning the fixed real constants for each constructor.
why it matters
This definition supports the downstream theorem fcc_hcp_denser_than_bcc that establishes higher packing for close-packed lattices than BCC, aligning with the module's RS mechanism of 8-tick coherence and the T7 eight-tick octave landmark. It supplies the numerical values used to compare densities in metallic bonding predictions, where higher coordination correlates with lower recognition cost.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.