`packingEfficiencyApprox`

definition

show as: view math explainer →

module: IndisputableMonolith.Chemistry.CrystalStructure
domain: Chemistry
line: 60 · 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 60.

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

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

papers checked against this theorem

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