eightTickCoherence

formal source

 137
 138/-- BCC is favored when 8-tick coherence dominates.
 139    The coordination number 8 directly reflects ledger periodicity. -/
 140def eightTickCoherence : Structure → ℝ
 141| .BCC => 1.0      -- Perfect 8-tick match
 142| .FCC => 2/3      -- 8/12 = 2/3 match
 143| .HCP => 2/3      -- Same as FCC
 144
 145/-- BCC has maximum 8-tick coherence. -/
 146theorem bcc_max_8tick_coherence :
 147    eightTickCoherence .BCC > eightTickCoherence .FCC ∧
 148    eightTickCoherence .BCC > eightTickCoherence .HCP := by
 149  simp only [eightTickCoherence]
 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