alkali_prefer_bcc
plain-language theorem explainer
Alkali metals with atomic numbers 3, 11, 19, 37 and 55 are classified inside the set of species that prefer body-centered cubic lattices. Materials scientists working inside the Recognition Science framework cite the result when assigning crystal structures to metals whose bonding is dominated by the eight-tick ledger period. The proof reduces to a single decide tactic that checks membership against an explicitly enumerated finite list.
Claim. For every integer atomic number $Z$, if $Z$ belongs to the set containing 3, 11, 19, 37 and 55, then $Z$ belongs to the set of atomic numbers whose elements prefer the body-centered cubic structure.
background
The CrystalStructure module derives lattice preferences from the eight-tick coordination rule: BCC lattices realize coordination number 8, matching the ledger period, while FCC and HCP realize coordination 12. The definition prefersBCC enumerates the metals in which this 8-tick coherence is strongest, explicitly including the alkali series together with Fe, Cr, W and Mo. The module states that packing efficiency then orders the structures as FCC ≈ HCP > BCC.
proof idea
The proof is a one-line wrapper that invokes the decide tactic on the membership predicate. Both the input list of alkali numbers and the target prefersBCC list are finite and ground, so the universal quantifier reduces to a decidable Boolean that evaluates to true by exhaustive enumeration.
why it matters
The theorem supplies the concrete chemical instance of the 8-tick coherence claim inside CM-001. It records that the alkali metals realize the strongest 8-tick dominance and therefore occupy the BCC class. The result sits directly under the eight-tick octave landmark (T7) and supplies the classification step that later packing-efficiency comparisons in the same module can reference.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.