packingEfficiencyApprox

formal source

  57| .HCP => Real.pi / (3 * Real.sqrt 2) -- ≈ 0.74
  58
  59/-- Approximate packing efficiency values. -/
  60def packingEfficiencyApprox : Structure → ℝ
  61| .BCC => 0.68
  62| .FCC => 0.74
  63| .HCP => 0.74
  64
  65/-- BCC coordination equals 8-tick. -/
  66theorem bcc_is_8_tick : coordination .BCC = 8 := rfl
  67
  68/-- FCC and HCP have coordination 12. -/
  69theorem close_packed_coordination : coordination .FCC = 12 ∧ coordination .HCP = 12 := by
  70  constructor <;> rfl
  71
  72/-- BCC has lower packing than FCC/HCP. -/
  73theorem bcc_packing_lt_fcc : packingEfficiencyApprox .BCC < packingEfficiencyApprox .FCC := by
  74  simp only [packingEfficiencyApprox]
  75  norm_num
  76
  77/-- FCC and HCP have same packing. -/
  78theorem fcc_hcp_same_packing : packingEfficiencyApprox .FCC = packingEfficiencyApprox .HCP := rfl
  79
  80/-! ## HCP c/a Ratio and φ Connection -/
  81
  82/-- Ideal c/a ratio for HCP: √(8/3) ≈ 1.633. -/
  83def idealHCPRatio : ℝ := Real.sqrt (8/3)
  84
  85/-- The ideal HCP c/a ratio is approximately 1.633. -/
  86theorem ideal_hcp_ratio_value : 1.63 < idealHCPRatio ∧ idealHCPRatio < 1.64 := by
  87  -- √(8/3) ≈ 1.6329931..., so 1.63 < √(8/3) < 1.64
  88  -- We verify: 1.63² = 2.6569 < 8/3 ≈ 2.6667 < 2.6896 = 1.64²
  89  simp only [idealHCPRatio]
  90  have h_sq_lo : (1.63 : ℝ)^2 < 8/3 := by norm_num