close_packed_12
plain-language theorem explainer
The coordination numbers for face-centered cubic and hexagonal close-packed lattices both equal 12. Materials scientists comparing metallic lattice stabilities or packing densities would cite this when deriving conductivity proxies from valence electron count. The proof is a one-line term wrapper that splits the conjunction via constructor and matches each side by reflexivity against the explicit definition values.
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 metallic bonding derivation, electron delocalization across a lattice of cations minimizes recognition cost (J-cost) and produces an 8-tick coherent many-body state. The module therefore predicts that metals exhibit high coordination numbers together with low ionization energy. The upstream definition of coordinationNumber maps each lattice type to a natural number: body-centered cubic receives 8 while both face-centered cubic and hexagonal close-packed receive 12.
proof idea
The proof is a one-line term-mode wrapper. Constructor splits the conjunction into two independent goals; reflexivity then discharges each equality because the definition of coordinationNumber returns 12 verbatim for the .FCC and .HCP cases.
why it matters
This result supplies the coordination numbers required by the module's prediction that metals are characterized by high coordination. It sits inside the Recognition Science 8-tick coherence picture and supports later comparisons of packing efficiency between close-packed and body-centered cubic structures. No downstream uses are recorded, yet the datum directly feeds any derivation of conductivity or thermal scaling that begins from lattice geometry.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.