bcc_coordination_8
plain-language theorem explainer
The declaration asserts that coordination number 8 lies inside the allowed set [8,12] for body-centered cubic structures. Crystallographers classifying Bravais lattices would cite it when confirming BCC nearest-neighbor shells. The proof is a direct decision procedure that checks finite-list membership.
Claim. In the body-centered cubic lattice the first coordination shell satisfies $8$ belonging to the allowed coordination numbers $[8,12]$.
background
The module derives the 32 crystallographic point groups and 7 crystal systems from the 8-tick structure that forces three spatial dimensions. Space-filling constraints then restrict rotations to orders 1, 2, 3, 4 and 6; the seven systems (triclinic through cubic) follow by clustering essential symmetry elements. Body-centered cubic belongs to the cubic system and exhibits coordination number 8, while face-centered cubic exhibits 12.
proof idea
The proof is a one-line wrapper that applies the decide tactic to the membership statement 8 ∈ [8,12].
why it matters
The result anchors the cubic Bravais lattices inside the RS derivation of crystal symmetry (CM-003). It links the eight-tick octave (T7) directly to observable coordination shells and supports the module's prediction of exactly 14 Bravais lattices. No downstream theorems are recorded yet.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.