packingEfficiencyApprox
plain-language theorem explainer
Approximate packing efficiencies assign 0.68 to BCC and 0.74 to both FCC and HCP. Researchers comparing RS crystal stability cite these constants when weighting packing density against 8-tick coherence in stability calculations. The definition implements a direct case split on the three constructors of the Structure inductive type.
Claim. The approximate packing efficiency function maps each crystal structure $s$ to a real number via the cases $s = $ BCC gives 0.68, $s = $ FCC gives 0.74, and $s = $ HCP gives 0.74.
background
The module defines Structure as an inductive type whose constructors are BCC, FCC, and HCP. The sibling coordination definition returns 8 for BCC and 12 for FCC or HCP, tying the numbers to the tick constant set to 1 in Constants. Packing efficiency approximates the fraction of space filled by spheres in each lattice arrangement.
proof idea
The definition is a direct pattern match on the Structure inductive type that returns the listed real constants for each constructor. No lemmas or tactics are invoked.
why it matters
This definition supplies the numerical values required by bcc_packing_lt_fcc, fcc_hcp_same_packing, stabilityScore, and stability_tradeoff. It realizes the packing prediction stated in the module documentation: FCC = HCP ≈ 0.74 > BCC ≈ 0.68. The assignment supports tradeoff analysis between packing weight and coherence weight, linking to the eight-tick octave.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.