  38open Constants
  39
  40/-- Crystal structure types. -/
  41inductive Structure
  42| BCC  -- Body-centered cubic
  43| FCC  -- Face-centered cubic
  44| HCP  -- Hexagonal close-packed
  45deriving Repr, DecidableEq
  46
  47/-- Coordination number for each structure. -/
  48def coordination : Structure → ℕ
  49| .BCC => 8
  50| .FCC => 12
  51| .HCP => 12
  52
  53/-- Packing efficiency (fraction of space filled by spheres). -/
  54def packingEfficiency : Structure → ℝ
  55| .BCC => Real.pi * Real.sqrt 3 / 8  -- ≈ 0.68
  56| .FCC => Real.pi / (3 * Real.sqrt 2) -- ≈ 0.74
  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

papers checked against this theorem

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