bcc_8tick
plain-language theorem explainer
The declaration establishes that body-centered cubic lattices carry a coordination number of eight, aligning with the eight-tick coherence required for metallic electron delocalization. Chemists working in Recognition Science would cite it when connecting lattice geometry to collective J-cost minimization. The proof is a one-line reflexivity that matches the definition of coordinationNumber directly on the BCC constructor.
Claim. The coordination number of the body-centered cubic lattice equals 8.
background
The module derives metallic bonding from delocalized valence electrons that minimize recognition cost across a cation lattice. It introduces an 8-tick coherence rhythm for the collective electron sea and links conductivity to free-electron density. The upstream definition coordinationNumber : LatticeType → ℕ maps .BCC to 8, .FCC to 12 and .HCP to 12; the sibling coordination definition in CrystalStructure supplies the same numeric values for the underlying Structure type.
proof idea
The proof is a one-line reflexivity that applies the definition of coordinationNumber to the .BCC case and returns the literal 8.
why it matters
This anchors the CH-011 metallic-bonding derivation to the eight-tick octave (T7) of the forcing chain. It supplies the high coordination number predicted for metals with low ionization energy and supports later statements on packing efficiency and conductivity proxies. No downstream theorems are listed, leaving the result as a direct interface between lattice geometry and the RS 8-tick mechanism.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.