fcc_hcp_same_packing
plain-language theorem explainer
FCC and HCP lattices receive identical approximate packing efficiencies of 0.74 in the Recognition Science assignment. Materials physicists comparing cohesive energies of close-packed metals cite this equality to rank FCC and HCP above BCC. The proof is a direct reflexivity step on the definition that maps both structures to the same numerical value.
Claim. The approximate packing efficiency of the face-centered cubic lattice equals the approximate packing efficiency of the hexagonal close-packed lattice.
background
Crystal structures emerge from the eight-tick coordination ledger and close-packing constraints. The function packingEfficiencyApprox assigns 0.68 to BCC and 0.74 to both FCC and HCP, matching the module statement that FCC and HCP reach maximum packing of approximately 74 percent with coordination 12 while BCC has coordination 8. Upstream results supply the explicit case values used in the equality.
proof idea
The proof is a one-line reflexivity application on the definition of packingEfficiencyApprox, which returns the same value 0.74 for the FCC and HCP cases.
why it matters
This equality supports the energy ordering FCC ≈ HCP > BCC within the crystal stability framework. It fills the module prediction that the two close-packed structures share packing efficiency, consistent with the eight-tick octave and phi-stability for the HCP c/a ratio near 1.633. No open questions are touched.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.