close_packed_coordination
plain-language theorem explainer
The theorem asserts that both the face-centered cubic and hexagonal close-packed lattices possess coordination number 12. Materials theorists working in Recognition Science would cite it when establishing the maximum-packing baseline that distinguishes close-packed phases from the 8-tick BCC structure. The proof is a one-line term wrapper that splits the conjunction and reduces each side by reflexivity on the structure definitions.
Claim. The coordination number of the face-centered cubic lattice equals 12 and the coordination number of the hexagonal close-packed lattice equals 12.
background
In the Crystal Structure Stability module, BCC, FCC, and HCP lattices are derived from the eight-tick ledger period and close-packing constraints. The coordination definition assigns 8 to BCC (reflecting the 8-tick octave) and 12 to both FCC and HCP (achieving the maximum packing fraction of approximately 74 percent). The module documentation states that FCC and HCP differ only in stacking sequence while sharing this coordination value, with HCP further constrained by an ideal c/a ratio near phi.
proof idea
The proof is a one-line term wrapper. Constructor splits the conjunction into two independent goals; rfl then discharges each goal by reflexivity against the defining clauses of the coordination function.
why it matters
This declaration supplies the explicit coordination values predicted in the module for the close-packed phases, supporting the energy ordering FCC approximately equal to HCP greater than BCC. It directly instantiates the framework landmark that eight-tick coherence favors BCC while maximum packing favors coordination 12. No downstream theorems are recorded, leaving open the quantitative link to cohesive-energy differences.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.