`coordination`

definition

show as: view math explainer →

module: IndisputableMonolith.Chemistry.CrystalStructure
domain: Chemistry
line: 48 · github
papers citing: none yet

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.Chemistry.CrystalStructure on GitHub at line 48.

browse module

All declarations in this module, on Recognition.

explainer page

Tracked in the explainer inventory; generation is lazy so crawlers do not trigger LLM jobs.

open explainer

depends on

used by

formal source

  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
  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

papers checked against this theorem

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