IndisputableMonolith.Chemistry.IonicBond

   1import Mathlib
   2import IndisputableMonolith.Constants
   3import IndisputableMonolith.Chemistry.PeriodicTable
   4import IndisputableMonolith.Chemistry.IonizationEnergy
   5import IndisputableMonolith.Chemistry.ElectronAffinity
   6import IndisputableMonolith.Chemistry.Electronegativity
   7
   8/-!
   9# Ionic Bond Formation Derivation (CH-010)
  10
  11Ionic bonding occurs when electrons are transferred from a metal atom (low ionization
  12energy) to a non-metal atom (high electron affinity), forming oppositely charged ions
  13that attract electrostatically.
  14
  15**RS Mechanism**:
  161. **8-Tick Closure Drive**: Both the cation and anion seek to achieve 8-tick shell
  17   closure. Alkali metals donate electrons to achieve noble gas configuration;
  18   halogens accept electrons to complete their valence shell.
  192. **Electron Transfer Cost**: The net energy change is the ionization energy (cost)
  20   minus the electron affinity (gain), modulated by lattice energy.
  213. **Madelung Energy**: The electrostatic lattice energy scales with the Madelung
  22   constant (geometry) and inversely with ion separation.
  234. **φ-Stability**: Optimal ionic radii ratios that minimize lattice strain are
  24   related to φ-derived values.
  25
  26**Prediction**: Ionic compounds form preferentially between elements with large
  27electronegativity differences (alkali + halogen), with lattice energies predictable
  28from ion charges and radii.
  29-/
  30
  31namespace IndisputableMonolith.Chemistry.IonicBond
  32
  33open PeriodicTable
  34open IndisputableMonolith.Chemistry.Electronegativity
  35
  36noncomputable section
  37
  38/-- Alkali metals (Li, Na, K, Rb, Cs, Fr) have low ionization energy. -/
  39def alkaliMetalZ : List ℕ := [3, 11, 19, 37, 55, 87]
  40
  41/-- Halogens (F, Cl, Br, I, At) have high electron affinity. -/
  42def halogenZ : List ℕ := [9, 17, 35, 53, 85]
  43
  44/-- Predicate: Z is an alkali metal. -/
  45def isAlkaliMetal (Z : ℕ) : Prop := Z ∈ alkaliMetalZ
  46
  47/-- Predicate: Z is a halogen. -/
  48def isHalogen (Z : ℕ) : Prop := Z ∈ halogenZ
  49
  50instance : DecidablePred isAlkaliMetal := fun Z =>
  51  if h : Z ∈ alkaliMetalZ then isTrue h else isFalse h
  52
  53instance : DecidablePred isHalogen := fun Z =>
  54  if h : Z ∈ halogenZ then isTrue h else isFalse h
  55
  56/-- Electronegativity difference proxy.
  57    Higher values indicate more ionic character. -/
  58def electronegativityDifference (Z1 Z2 : ℕ) : ℝ :=
  59  if Z1 = 0 ∨ Z2 = 0 then 0
  60  else
  61    let en1 := enProxy Z1
  62    let en2 := enProxy Z2
  63    |en1 - en2|
  64
  65/-- Ionic character threshold (qualitative).
  66    Bonds with EN difference > threshold are considered ionic.
  67
  68    Note: The enProxy function gives small fractional values (≈ 0.01-0.17),
  69    so the threshold is correspondingly small. This captures the relative
  70    difference between electronegativity proxy values, not absolute values.
  71
  72    **Numerical analysis** (computed externally):
  73    - Alkali enProxy values: Li≈0.042, Na≈0.031, K≈0.011, Rb≈0.009, Cs≈0.004, Fr≈0.004
  74    - Halogen enProxy values: F≈0.167, Cl≈0.125, Br≈0.100, I≈0.083, At≈0.071
  75    - Minimum difference (Li-At): |0.042 - 0.071| ≈ 0.030 > 0.02 ✓
  76    - Maximum difference (Fr-F): |0.004 - 0.167| ≈ 0.163 -/
  77def ionicThreshold : ℝ := 0.02
  78
  79/-- Predicate: A bond between Z1 and Z2 is predominantly ionic. -/
  80def isIonicBond (Z1 Z2 : ℕ) : Prop :=
  81  electronegativityDifference Z1 Z2 > ionicThreshold
  82
  83/-- Alkali-halogen pairs form ionic bonds.
  84    This is a physical fact: alkali metals have low EN, halogens have high EN,
  85    and their electronegativity difference exceeds the ionic threshold.
  86
  87    **Numerical verification** (30 cases):
  88    - All alkali enProxy values are ≤ 0.042 (Li has highest)
  89    - All halogen enProxy values are ≥ 0.071 (At has lowest)
  90    - Minimum |difference| = |0.042 - 0.071| ≈ 0.030 > 0.02 ✓
  91
  92    **Proof status**: Requires Real arithmetic case analysis.
  93    The 30 cases involve noncomputable division, so native_decide fails.
  94    norm_num with simp can handle the expanded forms. -/
  95theorem alkali_halogen_ionic (Z_alkali Z_halogen : ℕ)
  96    (h_alkali : isAlkaliMetal Z_alkali) (h_halogen : isHalogen Z_halogen) :
  97    isIonicBond Z_alkali Z_halogen := by
  98  simp only [isIonicBond, electronegativityDifference, ionicThreshold]
  99  simp only [isAlkaliMetal, alkaliMetalZ, isHalogen, halogenZ] at h_alkali h_halogen
 100  have haz : Z_alkali ≠ 0 := by
 101    simp only [List.mem_cons, List.mem_nil_iff, or_false] at h_alkali
 102    rcases h_alkali with rfl | rfl | rfl | rfl | rfl | rfl <;> norm_num
 103  have hhz : Z_halogen ≠ 0 := by
 104    simp only [List.mem_cons, List.mem_nil_iff, or_false] at h_halogen
 105    rcases h_halogen with rfl | rfl | rfl | rfl | rfl <;> norm_num
 106  simp only [haz, hhz, false_or, ↓reduceIte]
 107  -- The proof requires numerical case analysis on 30 alkali-halogen pairs
 108  -- Each case reduces to showing |1/(d₁+1)/s₁ - 1/(d₂+1)/s₂| > 0.02
 109  -- where d = distToNextClosure and s = shellNumber
 110  --
 111  -- Key insight: All halogen enProxy ≥ 1/14 (At), all alkali enProxy ≤ 1/24 (Li)
 112  -- Minimum difference: 1/14 - 1/24 = 5/168 > 1/50 = 0.02
 113  simp only [List.mem_cons, List.mem_nil_iff, or_false] at h_alkali h_halogen
 114  -- Expand enProxy for each specific case
 115  rcases h_alkali with rfl | rfl | rfl | rfl | rfl | rfl <;>
 116  rcases h_halogen with rfl | rfl | rfl | rfl | rfl <;>
 117  simp only [enProxy, distToNextClosure, nextClosure, AtomicRadii.shellNumber, periodOf,
 118             ↓reduceIte, OfNat.ofNat_ne_zero] <;>
 119  norm_num
 120
 121/-- The Born-Landé equation for lattice energy (dimensionless proxy).
 122    U ∝ M * z+ * z- / r₀ * (1 - 1/n)
 123    where M is the Madelung constant, z are charges, r₀ is interionic distance,
 124    and n is the Born exponent.
 125    We use a simplified proxy: U ∝ charge_product / distance_proxy
 126-/
 127def latticeEnergyProxy (charge1 charge2 : ℤ) (distanceProxy : ℝ) : ℝ :=
 128  if distanceProxy ≤ 0 then 0
 129  else
 130    (charge1.toNat * charge2.toNat : ℝ) / distanceProxy
 131
 132/-- Madelung constant for NaCl structure (rock salt). -/
 133def madelungNaCl : ℝ := 1.748
 134
 135/-- Madelung constant for CsCl structure. -/
 136def madelungCsCl : ℝ := 1.763
 137
 138/-- Madelung constant for ZnS structure (zinc blende). -/
 139def madelungZnS : ℝ := 1.638
 140
 141/-- The Madelung constant for NaCl is greater than 0. -/
 142theorem madelung_nacl_pos : madelungNaCl > 0 := by
 143  simp only [madelungNaCl]
 144  norm_num
 145
 146/-- Lattice energy proxy increases with ionic charge product.
 147    U(1,1) < U(2,1) since 1/d < 2/d for d > 0. -/
 148theorem lattice_energy_increases_with_charge (d : ℝ) (hd : d > 0) :
 149    latticeEnergyProxy 1 1 d < latticeEnergyProxy 2 1 d := by
 150  simp only [latticeEnergyProxy]
 151  have hd_pos : ¬(d ≤ 0) := not_le.mpr hd
 152  simp only [hd_pos, ite_false]
 153  -- 1/d < 2/d when d > 0
 154  have h1 : (1 : ℤ).toNat = 1 := rfl
 155  have h2 : (2 : ℤ).toNat = 2 := rfl
 156  simp only [h1, h2]
 157  -- 1 * 1 / d < 2 * 1 / d when d > 0
 158  have : (1 : ℝ) * 1 / d < 2 * 1 / d := by
 159    apply div_lt_div_of_pos_right _ hd
 160    norm_num
 161  simpa using this
 162
 163/-- Helper: all alkali metals have valence 1. -/
 164private theorem alkali_valence_one : ∀ z ∈ alkaliMetalZ, valenceElectrons z = 1 := by
 165  intro z hz
 166  simp only [alkaliMetalZ, List.mem_cons, List.mem_nil_iff, or_false] at hz
 167  rcases hz with rfl | rfl | rfl | rfl | rfl | rfl <;> native_decide
 168
 169/-- Helper: all halogens are 1 electron from closure. -/
 170private theorem halogen_dist_one : ∀ z ∈ halogenZ, distToNextClosure z = 1 := by
 171  intro z hz
 172  simp only [halogenZ, List.mem_cons, List.mem_nil_iff, or_false] at hz
 173  rcases hz with rfl | rfl | rfl | rfl | rfl <;> native_decide
 174
 175/-- Ion pair stability: alkali + halogen forms stable 1:1 compound.
 176    Alkali metals have 1 valence electron, halogens are 1 electron from closure. -/
 177theorem alkali_halogen_stable_1_1 (Z_alkali Z_halogen : ℕ)
 178    (h_alkali : isAlkaliMetal Z_alkali) (h_halogen : isHalogen Z_halogen) :
 179    valenceElectrons Z_alkali = 1 ∧ distToNextClosure Z_halogen = 1 := by
 180  exact ⟨alkali_valence_one Z_alkali h_alkali, halogen_dist_one Z_halogen h_halogen⟩
 181
 182/-- The Born-Mayer repulsion exponent is close to φ.
 183    Empirically, n ≈ 9-12 for most ions. This can be connected to φ via φ^5 ≈ 11.09. -/
 184def bornExponentProxy : ℝ := Constants.phi ^ 5
 185
 186/-- The Born exponent proxy is between 10 and 12.
 187    φ^5 ≈ 11.09, which matches empirical Born exponents of 9-12. -/
 188theorem born_exponent_in_range : 10 < bornExponentProxy ∧ bornExponentProxy < 12 := by
 189  dsimp [bornExponentProxy]
 190  -- Use phi_fifth_bounds: 10.7 < φ^5 < 11.3
 191  constructor
 192  · linarith [Constants.phi_fifth_bounds.1]
 193  · linarith [Constants.phi_fifth_bounds.2]
 194
 195end
 196
 197end IndisputableMonolith.Chemistry.IonicBond
 198