close_packed_lower_energy
plain-language theorem explainer
Close-packed FCC and HCP lattices carry lower energy scales than BCC under the Recognition Science assignment. A materials modeler comparing metallic cohesion would invoke this ordering when ranking lattice stabilities. The proof is a direct term reduction that unfolds the energyScale definition and checks the resulting numerical inequalities.
Claim. Let $E$ denote the dimensionless energy scale assigned to each crystal structure. Then $E_{FCC} < E_{BCC}$ and $E_{HCP} < E_{BCC}$, where $E_{BCC} = 1$ and $E_{FCC} = E_{HCP} = 0.917$ (the ratio of BCC to close-packed packing fractions).
background
The CrystalStructure module defines coordination numbers directly from the eight-tick ledger: BCC receives coordination 8 while FCC and HCP receive 12. The energyScale function is defined to be inversely related to packing efficiency, returning 1.0 for BCC and 0.917 for the two close-packed structures. This assignment implements the module's stated RS mechanism that close-packing lowers cohesive energy relative to 8-tick coordination.
proof idea
The term proof unfolds energyScale on each constructor, then applies constructor to split the conjunction and norm_num to discharge the two strict inequalities 0.917 < 1.0.
why it matters
The result ratifies the energy-ordering prediction listed under CM-001: FCC ≈ HCP > BCC. It directly ties the T7 eight-tick octave to lattice preference by making coordination number control the energyScale value. No downstream theorems are recorded, leaving the link to explicit phi-ladder mass formulas open.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.