`coordinationNumber`

definition

show as: view math explainer →

module: IndisputableMonolith.Chemistry.MetallicBond
domain: Chemistry
line: 81 · github
papers citing: none yet

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.Chemistry.MetallicBond on GitHub at line 81.

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

  78deriving Repr, DecidableEq
  79
  80/-- Coordination number for each lattice type. -/
  81def coordinationNumber : LatticeType → ℕ
  82| .BCC => 8
  83| .FCC => 12
  84| .HCP => 12
  85
  86/-- Packing efficiency for each lattice type. -/
  87def packingEfficiency : LatticeType → ℝ
  88| .BCC => 0.68
  89| .FCC => 0.74
  90| .HCP => 0.74
  91
  92/-- BCC has coordination number 8 (matching 8-tick). -/
  93theorem bcc_8tick : coordinationNumber .BCC = 8 := rfl
  94
  95/-- Close-packed structures (FCC, HCP) have coordination 12. -/
  96theorem close_packed_12 : coordinationNumber .FCC = 12 ∧ coordinationNumber .HCP = 12 := by
  97  constructor <;> rfl
  98
  99/-- FCC/HCP have higher packing efficiency than BCC. -/
 100theorem fcc_hcp_denser_than_bcc :
 101    packingEfficiency .BCC < packingEfficiency .FCC ∧
 102    packingEfficiency .BCC < packingEfficiency .HCP := by
 103  constructor <;> { simp only [packingEfficiency]; norm_num }
 104
 105/-- Metals have low ionization energy (alkali metals are easiest to ionize). -/
 106theorem alkali_low_ionization (Z : ℕ) (h : Z ∈ alkaliMetalZ) :
 107    valenceElectrons Z = 1 := by
 108  simp only [alkaliMetalZ] at h
 109  -- alkaliMetalZ = [3, 11, 19, 37, 55, 87]
 110  -- Each alkali metal: Z - prevClosure Z = 1
 111  fin_cases h <;> native_decide

papers checked against this theorem

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