fcc_hcp_same_packing
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.
claimThe 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 in Recognition Science
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.
scope and limits
- Does not derive exact packing fractions from first principles.
- Does not model real-material deviations from ideal ratios.
- Does not address crystal types outside BCC, FCC, and HCP.
formal statement (Lean)
78theorem fcc_hcp_same_packing : packingEfficiencyApprox .FCC = packingEfficiencyApprox .HCP := rfl
proof body
Term-mode proof.
79
80/-! ## HCP c/a Ratio and φ Connection -/
81
82/-- Ideal c/a ratio for HCP: √(8/3) ≈ 1.633. -/