IndisputableMonolith.Chemistry.ElectronAffinity

   1import Mathlib
   2import IndisputableMonolith.Constants
   3import IndisputableMonolith.Chemistry.PeriodicTable
   4
   5/-!
   6# Electron Affinity from φ-Ladder Scaling (CH-006)
   7
   8Electron affinity (EA) measures the energy released when adding an electron.
   9RS predicts EA follows the "approach to closure" pattern:
  10
  111. **Halogens** (one electron from closure) have HIGH EA
  122. **Noble gases** (at closure) have NEAR-ZERO or NEGATIVE EA
  133. **Alkali metals** (one past closure) have LOW EA
  14
  15**RS Mechanism**: EA = cost reduction from approaching 8-tick neutrality.
  16Adding an electron to a halogen completes a shell (low cost → high EA).
  17Adding an electron to a noble gas starts a new shell (high cost → low/negative EA).
  18
  19**Key predictions**:
  20- EA ordering: Halogens > Chalcogens > Pnictogens > ... > Noble gases
  21- Sign prediction: Noble gases have EA ≤ 0
  22- Halogen maximum within each period
  23-/
  24
  25namespace IndisputableMonolith
  26namespace Chemistry
  27namespace ElectronAffinity
  28
  29open PeriodicTable
  30
  31noncomputable section
  32
  33/-- Distance to next noble gas closure (electrons needed to complete shell).
  34    This is the fundamental proxy for electron affinity. -/
  35def distToClosure (Z : ℕ) : ℕ := distToNextClosure Z
  36
  37/-- Electron affinity proxy: higher when closer to closure.
  38    EA_proxy = periodLength - valenceElectrons = distToClosure
  39    Halogens (dist=1) have highest proxy, noble gases (dist=0) have lowest. -/
  40def eaProxy (Z : ℕ) : ℕ := distToClosure Z
  41
  42/-- Normalized EA proxy: fraction of shell remaining.
  43    EA_norm = distToClosure / periodLength ∈ [0, 1)
  44    Higher = more favorable to add electron. -/
  45def normalizedEA (Z : ℕ) : ℝ :=
  46  if periodLength Z = 0 then 0
  47  else (distToClosure Z : ℝ) / (periodLength Z : ℝ)
  48
  49/-- Predicate: element is a halogen (one electron from noble gas closure). -/
  50def isHalogen (Z : ℕ) : Prop := distToClosure Z = 1
  51
  52/-- Halogen set: {9, 17, 35, 53, 85}. -/
  53def halogenZ : List ℕ := [9, 17, 35, 53, 85]
  54
  55/-- Decidable instance for halogen membership. -/
  56instance : DecidablePred isHalogen := fun Z =>
  57  if h : distToClosure Z = 1 then isTrue h else isFalse h
  58
  59/-! ## Sign Predictions -/
  60
  61/-- Noble gases have EA proxy = 0 (at closure, no benefit from adding electron). -/
  62theorem noble_gas_ea_zero (Z : ℕ) (h : isNobleGas Z) : eaProxy Z = 0 := by
  63  simp only [eaProxy, distToClosure]
  64  exact noble_gas_at_closure Z h
  65
  66/-- Halogens have EA proxy = 1 (one electron completes shell). -/
  67theorem halogen_ea_one (Z : ℕ) (h : isHalogen Z) : eaProxy Z = 1 := by
  68  simp only [eaProxy, distToClosure]
  69  exact h
  70
  71/-- Fluorine is a halogen (in list). -/
  72theorem fluorine_in_halogen_list : 9 ∈ halogenZ := by native_decide
  73
  74/-- Chlorine is a halogen (in list). -/
  75theorem chlorine_in_halogen_list : 17 ∈ halogenZ := by native_decide
  76
  77/-- Bromine is a halogen (in list). -/
  78theorem bromine_in_halogen_list : 35 ∈ halogenZ := by native_decide
  79
  80/-- Iodine is a halogen (in list). -/
  81theorem iodine_in_halogen_list : 53 ∈ halogenZ := by native_decide
  82
  83/-- Astatine is a halogen (in list). -/
  84theorem astatine_in_halogen_list : 85 ∈ halogenZ := by native_decide
  85
  86/-! ## Ordering Predictions -/
  87
  88/-- Within a period, EA proxy decreases as Z increases (filling the shell).
  89    Elements closer to closure have higher EA potential. -/
  90theorem ea_decreases_within_period (Z1 Z2 : ℕ)
  91    (hZ1le : Z1 ≤ nextClosure Z1)
  92    (hZ2le : Z2 ≤ nextClosure Z2)
  93    (hLt : Z1 < Z2)
  94    (hSame : nextClosure Z1 = nextClosure Z2) :
  95    eaProxy Z1 > eaProxy Z2 := by
  96  simp only [eaProxy, distToClosure, distToNextClosure]
  97  omega
  98
  99/-- Halogens have higher EA proxy than any other non-noble element in their period. -/
 100theorem halogen_max_ea (Z : ℕ) (Z' : ℕ)
 101    (hZle : Z ≤ nextClosure Z)
 102    (_ : Z' ≤ nextClosure Z')
 103    (hSamePeriod : nextClosure Z = nextClosure Z')
 104    (hZ'lt : Z' < nextClosure Z') :
 105    distToNextClosure Z' ≤ distToNextClosure Z ↔ Z ≤ Z' := by
 106  simp only [distToNextClosure]
 107  omega
 108
 109/-! ## Specific Element Theorems -/
 110
 111/-- Fluorine (Z=9) is a halogen. -/
 112theorem fluorine_is_halogen : isHalogen 9 := by native_decide
 113
 114/-- Chlorine (Z=17) is a halogen. -/
 115theorem chlorine_is_halogen : isHalogen 17 := by native_decide
 116
 117/-- Bromine (Z=35) is a halogen. -/
 118theorem bromine_is_halogen : isHalogen 35 := by native_decide
 119
 120/-- Iodine (Z=53) is a halogen. -/
 121theorem iodine_is_halogen : isHalogen 53 := by native_decide
 122
 123/-- Astatine (Z=85) is a halogen. -/
 124theorem astatine_is_halogen : isHalogen 85 := by native_decide
 125
 126/-- Neon (Z=10) has zero EA proxy. -/
 127theorem neon_ea_zero : eaProxy 10 = 0 := by native_decide
 128
 129/-- Argon (Z=18) has zero EA proxy. -/
 130theorem argon_ea_zero : eaProxy 18 = 0 := by native_decide
 131
 132/-! ## Falsification Criteria
 133
 134The electron affinity derivation is falsifiable:
 135
 1361. **Sign violation**: If noble gases have positive EA (they should be ≤ 0).
 137
 1382. **Halogen not maximum**: If any halogen does NOT have maximum EA in its period.
 139
 1403. **Ordering violation**: If EA ordering doesn't follow "closer to closure = higher EA"
 141   for main group elements (allowing d/f-block anomalies).
 142
 143Note: Actual EA values in eV are NOT predicted without a scale anchor.
 144Only the ORDERING and SIGNS are fit-free predictions.
 145-/
 146
 147end
 148end ElectronAffinity
 149end Chemistry
 150end IndisputableMonolith
 151