`conductivityProxy`

definition

show as: view math explainer →

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

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.Chemistry.MetallicBond on GitHub at line 69.

browse module

All declarations in this module, on Recognition.

explainer page

A cached Ask Recognition explainer exists for this declaration.

open explainer

depends on

formal source

  66
  67/-- Electrical conductivity proxy based on free electron density.
  68    Higher free electrons per atom → higher conductivity. -/
  69def conductivityProxy (Z : ℕ) : ℝ :=
  70  (freeElectrons Z : ℝ)
  71
  72/-- Coordination number in metallic lattices.
  73    BCC: 8, FCC/HCP: 12 -/
  74inductive LatticeType
  75| BCC  -- Body-centered cubic (coordination 8)
  76| FCC  -- Face-centered cubic (coordination 12)
  77| HCP  -- Hexagonal close-packed (coordination 12)
  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. -/

papers checked against this theorem

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