prefersBCC
This definition enumerates the atomic numbers of metals whose crystal structures favor body-centered cubic (BCC) coordination in the Recognition Science framework. Researchers modeling 8-tick coherence in solid-state physics would cite it when linking alkali and certain transition metals to the ledger period. The entry is a direct list definition with no computation or lemmas.
claimThe atomic numbers of metals preferring BCC crystal structures are $3$ (Li), $11$ (Na), $19$ (K), $37$ (Rb), $55$ (Cs), $26$ (Fe), $24$ (Cr), $74$ (W), and $42$ (Mo).
background
The CrystalStructure module derives BCC, FCC, and HCP lattices from RS principles. BCC coordination equals 8 because it matches the eight-tick ledger period (T7) in the Unified Forcing Chain, favoring metals with strong 8-tick coherence such as the alkali series. Close-packed structures achieve higher packing density but require coordination 12 and a c/a ratio near phi for HCP stability. Upstream constants include K defined as phi to the power 1/2 and W as the count of wallpaper groups supplying the symmetry basis for lattice classification.
proof idea
This is a direct definition of the list of atomic numbers. No lemmas or tactics are applied; the declaration simply enumerates the values for downstream use.
why it matters in Recognition Science
The definition supplies the concrete data for the theorem alkali_prefer_bcc, which shows that all alkali metals lie in this list. It implements the module prediction that BCC is selected when 8-tick coherence dominates, directly referencing T7 of the forcing chain. The entry closes the empirical bridge between the abstract ledger period and observed crystal preferences without introducing new hypotheses.
scope and limits
- Does not derive the listed atomic numbers from the phi-ladder or RCL within the proof.
- Does not address temperature or pressure dependence of structure selection.
- Does not claim that every element with these atomic numbers forms BCC under all conditions.
- Does not extend to non-metallic elements or alloys.
Lean usage
theorem alkali_prefer_bcc : ∀ Z, Z ∈ [3, 11, 19, 37, 55] → Z ∈ prefersBCC := by decideformal statement (Lean)
174def prefersBCC : List ℕ := [3, 11, 19, 37, 55, 26, 24, 74, 42] -- Li, Na, K, Rb, Cs, Fe, Cr, W, Mo
proof body
Definition body.
175
176/-- Metals that prefer FCC: Cu, Ag, Au, Al, Ni, Pb. -/