close_packed_coordination

formal source

  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
  91  have h_sq_hi : (8 : ℝ)/3 < (1.64 : ℝ)^2 := by norm_num
  92  constructor
  93  · -- 1.63 < √(8/3) ⟺ 1.63² < 8/3 (for positive values)
  94    rw [Real.lt_sqrt (by norm_num : (0 : ℝ) ≤ 1.63)]
  95    exact h_sq_lo
  96  · -- √(8/3) < 1.64 ⟺ 8/3 < 1.64² (for positive values)
  97    rw [Real.sqrt_lt' (by norm_num : (0 : ℝ) < 1.64)]
  98    exact h_sq_hi
  99