 150  constructor <;> norm_num
 151
 152/-- Stability is a balance of packing and 8-tick coherence. -/
 153def stabilityScore (s : Structure) (packing_weight coherence_weight : ℝ) : ℝ :=
 154  packing_weight * packingEfficiencyApprox s + coherence_weight * eightTickCoherence s
 155
 156/-- With high coherence weight, BCC wins; with very high packing weight, FCC wins.
 157    For FCC to beat BCC: 0.74p + 0.667c > 0.68p + 1.0c → 0.06p > 0.333c → p/c > 5.5
 158    So we need packing weight over 5× the coherence weight. -/
 159theorem stability_tradeoff :
 160    stabilityScore .BCC 0.3 0.7 > stabilityScore .FCC 0.3 0.7 ∧
 161    stabilityScore .FCC 0.9 0.1 > stabilityScore .BCC 0.9 0.1 := by
 162  simp only [stabilityScore, packingEfficiencyApprox, eightTickCoherence]
 163  -- BCC (0.3, 0.7): 0.3 * 0.68 + 0.7 * 1.0 = 0.204 + 0.7 = 0.904
 164  -- FCC (0.3, 0.7): 0.3 * 0.74 + 0.7 * (2/3) ≈ 0.222 + 0.467 = 0.689
 165  -- So BCC > FCC with high coherence weight ✓
 166  -- BCC (0.9, 0.1): 0.9 * 0.68 + 0.1 * 1.0 = 0.612 + 0.1 = 0.712
 167  -- FCC (0.9, 0.1): 0.9 * 0.74 + 0.1 * (2/3) = 0.666 + 0.067 ≈ 0.733
 168  -- So FCC > BCC with very high packing weight ✓
 169  constructor <;> norm_num
 170
 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

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.