coordinationNumber
The coordination number definition maps body-centered cubic lattices to 8 and both face-centered cubic and hexagonal close-packed lattices to 12. Chemists deriving packing and conductivity properties inside Recognition Science would cite these fixed values when linking metallic lattices to eight-tick coherence. The definition is realized by exhaustive case distinction on the three constructors of LatticeType.
claimLet $c :$ LatticeType $→ ℕ$ satisfy $c($BCC$) = 8$, $c($FCC$) = 12$, and $c($HCP$) = 12$.
background
LatticeType is the inductive type whose constructors are BCC (body-centered cubic), FCC (face-centered cubic), and HCP (hexagonal close-packed). The module derives metallic bonding from electron delocalization across a lattice of cations to minimize J-cost, together with collective 8-tick rhythm and φ-scaling of conductivity. Upstream, the LatticeType inductive is introduced in the same file while the forcing structure supplies the self-reference axioms that underwrite the coherence requirement.
proof idea
The definition proceeds by direct pattern matching on the three constructors of LatticeType, returning the constant natural numbers 8, 12, and 12. No lemmas or tactics are invoked; it is a pure case definition.
why it matters in Recognition Science
This definition supplies the numerical inputs to the downstream theorems bcc_8tick and close_packed_12, which connect coordination numbers to the eight-tick octave (T7) in the forcing chain. It fills the CH-011 step for metallic bonding by furnishing the coordination values that realize 8-tick coherence for BCC and denser packing for close-packed structures. It touches the open question of whether lattice stability itself follows from φ-scaling of recognition cost.
scope and limits
- Does not derive the three lattice types from the forcing chain.
- Does not compute packing efficiency or conductivity from these numbers.
- Does not assign coordination numbers to specific elements or Z values.
- Does not prove that the assigned numbers minimize J-cost.
formal statement (Lean)
81def coordinationNumber : LatticeType → ℕ
82| .BCC => 8
83| .FCC => 12
84| .HCP => 12
85
86/-- Packing efficiency for each lattice type. -/