Chemistry Metallic Bond Close Packed 12

The close-packed coordination number

In crystallography, a close-packed structure is one in which spheres of equal size are arranged to fill space as densely as possible. Two common arrangements achieve this: face-centered cubic (FCC) and hexagonal close-packed (HCP). In both, each sphere touches twelve neighbors, a number called the coordination number. The packing efficiency, the fraction of space occupied by the spheres, is 0.74 for both structures. Body-centered cubic (BCC), by contrast, has a coordination number of 8 and a packing efficiency of 0.68, making it a less dense arrangement.

The distinction matters for metallic bonding. Metals are often described as a lattice of positive ions immersed in a delocalized electron sea, a shared pool of valence electrons that conducts electricity and heat. The coordination number reflects how tightly the ions are packed, which influences properties such as density and mechanical strength. A higher coordination number generally means a more compact lattice and stronger metallic bonding per atom.

In Recognition Science, the framework models metallic lattices with a simple type: BCC, FCC, or HCP. Its machine-checked library of formal theorems contains a declaration named close_packed_12 that proves, by direct computation, that the coordination number of FCC is 12 and the coordination number of HCP is 12. This is a ledger, a discrete record of events, holding a fact about the framework's own definitions. The theorem does not derive the coordination number from physical principles; it verifies the number assigned in the framework's lattice model.

The library also proves that FCC and HCP have higher packing efficiency than BCC, again by direct computation from the defined values. These theorems are formal tautologies about the framework's model, not empirical discoveries about real metals. Real metals do exhibit coordination numbers of 12 in FCC and HCP lattices, but the framework's theorem does not establish that connection to measurement.

/-- Close-packed structures (FCC, HCP) have coordination 12. -/
theorem close_packed_12 : coordinationNumber .FCC = 12 ∧ coordinationNumber .HCP = 12 := by
  constructor <;> rfl

/-- FCC/HCP have higher packing efficiency than BCC. -/
theorem fcc_hcp_denser_than_bcc :
    packingEfficiency .BCC < packingEfficiency .FCC ∧
    packingEfficiency .BCC < packingEfficiency .HCP := by
  constructor <;> { simp only [packingEfficiency]; norm_num }

What this page does not claim

The theorem does not derive coordination number 12 from physical principles; it verifies a definitional assignment. The theorem does not establish that real FCC or HCP metals have coordination number 12; that is an empirical fact. The framework does not claim that its lattice model is the only valid description of metallic structure.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/Chemistry/MetallicBond.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red: