fcc_hcp_same_packing

formal source

  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
 100/-- The ideal HCP ratio is close to φ ≈ 1.618.
 101    √(8/3) ≈ 1.633, φ ≈ 1.618, difference ≈ 0.015.
 102    Using available bounds: 1.63 < √(8/3) < 1.64, 1.61 < φ < 1.62.
 103    This gives |√(8/3) - φ| < 1.64 - 1.61 = 0.03. -/
 104theorem hcp_ratio_near_phi : |idealHCPRatio - phi| < 0.03 := by
 105  simp only [idealHCPRatio]
 106  -- First establish that √(8/3) > φ, so |√(8/3) - φ| = √(8/3) - φ
 107  have h_phi_lt : phi < 1.62 := phi_lt_onePointSixTwo
 108  have h_163_lt_sqrt : (1.63 : ℝ) < Real.sqrt (8/3) := by