`packingEfficiency`

definition

show as: view math explainer →

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

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.Chemistry.CrystalStructure on GitHub at line 54.

browse module

All declarations in this module, on Recognition.

explainer page

A cached Ask Recognition explainer exists for this declaration.

open explainer

depends on

used by

formal source

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

papers checked against this theorem

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