`enProxy`

definition

show as: view math explainer →

module: IndisputableMonolith.Chemistry.Electronegativity
domain: Chemistry
line: 36 · github
papers citing: none yet

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.Chemistry.Electronegativity on GitHub at line 36.

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

  33/-- Electronegativity proxy based on distance to closure.
  34    EN ~ 1 / (distToNextClosure + 1) * (1 / shellNumber)
  35    Elements close to closure in small shells have high EN. -/
  36def enProxy (Z : ℕ) : ℝ :=
  37  if Z = 0 then 0
  38  else if distToNextClosure Z = 0 then 0  -- Noble gases undefined
  39  else (1 : ℝ) / ((distToNextClosure Z : ℝ) + 1) * (1 / (shellNumber Z : ℝ))
  40
  41/-- Simplified EN ranking: valenceElectrons / periodLength.
  42    Higher valence fraction = higher EN (within same shell). -/
  43def enRanking (Z : ℕ) : ℝ :=
  44  if periodLength Z = 0 then 0
  45  else (valenceElectrons Z : ℝ) / (periodLength Z : ℝ)
  46
  47/-! ## Ordering Predictions -/
  48
  49/-- Fluorine (Z=9) has higher EN ranking than Li. -/
  50theorem fluorine_gt_li : enRanking 9 > enRanking 3 := by
  51  simp only [enRanking, valenceElectrons, periodLength, prevClosure, nextClosure]; norm_num
  52
  53/-- Fluorine (Z=9) has higher EN ranking than Be. -/
  54theorem fluorine_gt_be : enRanking 9 > enRanking 4 := by
  55  simp only [enRanking, valenceElectrons, periodLength, prevClosure, nextClosure]; norm_num
  56
  57/-- Fluorine (Z=9) has higher EN ranking than B. -/
  58theorem fluorine_gt_b : enRanking 9 > enRanking 5 := by
  59  simp only [enRanking, valenceElectrons, periodLength, prevClosure, nextClosure]; norm_num
  60
  61/-- Fluorine (Z=9) has higher EN ranking than C. -/
  62theorem fluorine_gt_c : enRanking 9 > enRanking 6 := by
  63  simp only [enRanking, valenceElectrons, periodLength, prevClosure, nextClosure]; norm_num
  64
  65/-- Fluorine (Z=9) has higher EN ranking than N. -/
  66theorem fluorine_gt_n : enRanking 9 > enRanking 7 := by

papers checked against this theorem

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