IndisputableMonolith.Chemistry.Electronegativity

   1import Mathlib
   2import IndisputableMonolith.Constants
   3import IndisputableMonolith.Chemistry.PeriodicTable
   4import IndisputableMonolith.Chemistry.ElectronAffinity
   5import IndisputableMonolith.Chemistry.AtomicRadii
   6
   7/-!
   8# Electronegativity from φ-Ladder Scaling (CH-008)
   9
  10Electronegativity (EN) measures an atom's tendency to attract electrons.
  11RS predicts EN follows a pattern based on shell structure and distance to closure.
  12
  13**Classical relationship**: EN ~ √(IE × EA) (Mulliken scale)
  14**RS mechanism**: EN ~ distToNextClosure^(-1) modulated by shell number
  15
  16**Key predictions**:
  171. Fluorine (F) has highest EN (closest to closure in small shell)
  182. Noble gases have low/undefined EN (complete shells)
  193. EN increases across a period (approaching closure)
  204. EN decreases down a group (larger shells)
  215. Cesium/Francium have lowest EN (farthest from closure in large shells)
  22-/
  23
  24namespace IndisputableMonolith
  25namespace Chemistry
  26namespace Electronegativity
  27
  28open PeriodicTable
  29open AtomicRadii
  30
  31noncomputable section
  32
  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
  67  simp only [enRanking, valenceElectrons, periodLength, prevClosure, nextClosure]; norm_num
  68
  69/-- Fluorine (Z=9) has higher EN ranking than O. -/
  70theorem fluorine_gt_o : enRanking 9 > enRanking 8 := by
  71  simp only [enRanking, valenceElectrons, periodLength, prevClosure, nextClosure]; norm_num
  72
  73/-- Chlorine (Z=17) has higher EN ranking than Sodium (Z=11). -/
  74theorem chlorine_gt_sodium : enRanking 17 > enRanking 11 := by
  75  simp only [enRanking, valenceElectrons, periodLength, prevClosure, nextClosure]
  76  norm_num
  77
  78/-- EN increases across a period: valence electrons increase toward closure. -/
  79theorem en_increases_across_period (Z1 Z2 : ℕ)
  80    (hZ1_gt_prev : Z1 > prevClosure Z1)
  81    (hZ2_gt_prev : Z2 > prevClosure Z2)
  82    (hSamePrev : prevClosure Z1 = prevClosure Z2)
  83    (hLt : Z1 < Z2) :
  84    valenceElectrons Z1 < valenceElectrons Z2 := by
  85  simp only [valenceElectrons]
  86  omega
  87
  88/-! ## Group Trends -/
  89
  90/-- EN generally decreases down a group (larger shells reduce EN).
  91    Example: F > Cl in absolute EN (but ranking might be similar). -/
  92theorem group_17_en_order :
  93    shellNumber 9 < shellNumber 17 ∧ shellNumber 17 < shellNumber 35 := by
  94  native_decide
  95
  96/-- Alkali metals have lowest EN in their periods (valence = 1). -/
  97theorem alkali_min_valence :
  98    valenceElectrons 3 = 1 ∧ valenceElectrons 11 = 1 ∧ valenceElectrons 19 = 1 := by
  99  native_decide
 100
 101/-! ## Specific Element Theorems -/
 102
 103/-- Cesium (Z=55) has very low EN ranking. -/
 104theorem cesium_low_en : enRanking 55 < enRanking 9 := by
 105  simp only [enRanking, valenceElectrons, periodLength, prevClosure, nextClosure]
 106  norm_num
 107
 108/-- Carbon (Z=6) has intermediate EN (half-filled). -/
 109theorem carbon_intermediate : enRanking 6 = 1/2 := by
 110  simp only [enRanking, valenceElectrons, periodLength, prevClosure, nextClosure]
 111  norm_num
 112
 113/-- Nitrogen (Z=7) has EN ranking 5/8. -/
 114theorem nitrogen_ranking : enRanking 7 = 5/8 := by
 115  simp only [enRanking, valenceElectrons, periodLength, prevClosure, nextClosure]
 116  norm_num
 117
 118/-- Oxygen (Z=8) has EN ranking 6/8 = 3/4. -/
 119theorem oxygen_ranking : enRanking 8 = 3/4 := by
 120  simp only [enRanking, valenceElectrons, periodLength, prevClosure, nextClosure]
 121  norm_num
 122
 123/-- Fluorine (Z=9) has EN ranking 7/8. -/
 124theorem fluorine_ranking : enRanking 9 = 7/8 := by
 125  simp only [enRanking, valenceElectrons, periodLength, prevClosure, nextClosure]
 126  norm_num
 127
 128/-! ## Noble Gas EN -/
 129
 130/-- Noble gases have zero EN proxy (complete shells). -/
 131theorem noble_gas_zero_en (Z : ℕ) (h : isNobleGas Z) (hZ_pos : Z > 0) : enProxy Z = 0 := by
 132  simp only [enProxy]
 133  have h_dist : distToNextClosure Z = 0 := noble_gas_at_closure Z h
 134  have hZ_ne : Z ≠ 0 := by omega
 135  simp only [hZ_ne, h_dist, ↓reduceIte]
 136
 137/-! ## Falsification Criteria
 138
 139The electronegativity derivation is falsifiable:
 140
 1411. **Ordering violation**: If F is not highest EN or Cs is not among lowest.
 142
 1432. **Period trend violation**: If EN decreases across a period (opposite to prediction).
 144
 1453. **Group trend violation**: If EN increases going down a group (opposite to prediction).
 146
 147Note: Absolute EN values (Pauling units) are NOT predicted without calibration.
 148Only the ORDERING is a fit-free prediction.
 149-/
 150
 151end
 152end Electronegativity
 153end Chemistry
 154end IndisputableMonolith
 155