coordination
plain-language theorem explainer
Coordination numbers in the Recognition Science crystal model assign 8 neighbors to BCC structures and 12 to both FCC and HCP. Researchers modeling metallic bonding or lattice stability cite this definition to connect geometry to the eight-tick ledger period. The definition proceeds by exhaustive case analysis on the three Structure constructors.
Claim. Let $S$ be a crystal structure of type BCC, FCC or HCP. The coordination number $c(S)$ is defined by $c($BCC$) = 8$, $c($FCC$) = 12$, $c($HCP$) = 12$.
background
Crystal structures are classified into three types: body-centered cubic (BCC), face-centered cubic (FCC), and hexagonal close-packed (HCP). The module sets out how these emerge from RS principles, with BCC reflecting the 8-tick ledger period and FCC/HCP achieving close packing with coordination 12. The coordination function maps each structure type to its nearest-neighbor count. Upstream results include the Structure inductive definition together with structures from LedgerFactorization and PhiForcingDerived that calibrate the J-cost and forcing chains. From the module: 'BCC has coordination number 8, directly reflecting the 8-tick ledger period.'
proof idea
This is a definition by pattern matching on the Structure inductive type, assigning the constants 8, 12, and 12 to BCC, FCC, and HCP respectively. No lemmas are applied; it serves as the base for subsequent theorems that prove equalities by reflexivity.
why it matters
This definition supplies the numerical values used in theorems establishing the 8-tick connection for BCC and the lower energy of close-packed structures. It fills the CM-001 prediction that BCC coordination equals 8 and FCC/HCP equal 12, linking directly to the eight-tick octave in the forcing chain. Downstream results such as bcc_is_8_tick and close_packed_coordination rely on it for their reflexivity proofs.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.