def
definition
prefersBCC
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.Chemistry.CrystalStructure on GitHub at line 174.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
171/-! ## Metal Preferences -/
172
173/-- Metals that prefer BCC (8-tick dominant): alkali metals, Fe, Cr, W, Mo. -/
174def prefersBCC : List ℕ := [3, 11, 19, 37, 55, 26, 24, 74, 42] -- Li, Na, K, Rb, Cs, Fe, Cr, W, Mo
175
176/-- Metals that prefer FCC: Cu, Ag, Au, Al, Ni, Pb. -/
177def prefersFCC : List ℕ := [29, 47, 79, 13, 28, 82]
178
179/-- Metals that prefer HCP: Mg, Zn, Ti, Zr. -/
180def prefersHCP : List ℕ := [12, 30, 22, 40]
181
182/-- Alkali metals prefer BCC (strongest 8-tick coherence). -/
183theorem alkali_prefer_bcc : ∀ Z, Z ∈ [3, 11, 19, 37, 55] → Z ∈ prefersBCC := by
184 decide
185
186end
187
188end CrystalStructure
189end Chemistry
190end IndisputableMonolith