IndisputableMonolith.Chemistry.IonizationEnergy

   1import Mathlib
   2import IndisputableMonolith.Constants
   3import IndisputableMonolith.Chemistry.PeriodicTable
   4
   5/-!
   6# Ionization Energy from φ-Ladder Scaling (P0-A2)
   7
   8First ionization energy I₁(Z) measures the cost to remove one electron.
   9RS predicts this follows a sawtooth pattern forced by:
  10
  111. **φ-rail scaling**: Base energy scales as φ^{2n} for period n
  122. **Position factor**: Within a period, energy increases toward closure
  133. **Block offsets**: s/p/d/f subshells have fixed φ-packing offsets
  14
  15**Key predictions**:
  16- Alkali metals (valence = 1) have MINIMUM ionization energy per period
  17- Noble gases (valence = period length) have MAXIMUM ionization energy per period
  18- The sawtooth emerges WITHOUT fitting to data
  19
  20**Falsification**: If the predicted ordering (alkali < ... < noble within each period)
  21fails on a prereg'd element set, the model is falsified.
  22-/
  23
  24namespace IndisputableMonolith
  25namespace Chemistry
  26namespace IonizationEnergy
  27
  28open PeriodicTable
  29
  30noncomputable section
  31
  32/-- Dimensionless ionization energy proxy based on position in period.
  33    Runs from 1 (alkali) to periodLength (noble gas).
  34    This captures the "cost to break into a forming shell." -/
  35def ionizationProxy (Z : ℕ) : ℕ :=
  36  valenceElectrons Z
  37
  38/-- Period-normalized ionization: proxy / period length.
  39    Noble gases have value 1.0, alkali metals have value 1/n. -/
  40def normalizedIonization (Z : ℕ) : ℝ :=
  41  if periodLength Z = 0 then 0
  42  else (ionizationProxy Z : ℝ) / (periodLength Z : ℝ)
  43
  44/-- φ-scaled ionization energy (dimensionless).
  45    Combines rail factor with position factor.
  46    I_scaled(Z) = φ^{2·period} × (valence / periodLength) -/
  47def scaledIonization (Z : ℕ) : ℝ :=
  48  let period := periodOf Z
  49  let rf := Real.rpow Constants.phi ((2 : ℝ) * (period : ℝ))
  50  rf * normalizedIonization Z
  51
  52/-- Predicted ionization energy in eV (display seam).
  53    Uses E_coh as the universal energy anchor. -/
  54def predictedI1_eV (Z : ℕ) : ℝ :=
  55  Constants.E_coh * scaledIonization Z * 1000  -- Scale factor for eV range
  56
  57/-! ## Ordering Theorems (Sawtooth Structure) -/
  58
  59/-- Alkali metals have valence = 1 (one electron beyond noble gas core). -/
  60def isAlkaliMetal (Z : ℕ) : Prop :=
  61  valenceElectrons Z = 1 ∧ Z > 1  -- Excludes hydrogen
  62
  63/-- Alkali metal set: {3, 11, 19, 37, 55, 87}. -/
  64def alkaliMetalZ : List ℕ := [3, 11, 19, 37, 55, 87]
  65
  66/-- Within any period, alkali metals have minimum ionization proxy. -/
  67theorem alkali_min_ionization (Z : ℕ) (hZ : valenceElectrons Z = 1) (hZ2 : Z > 2) :
  68    ionizationProxy Z = 1 := by
  69  simp only [ionizationProxy]
  70  exact hZ
  71
  72/-- Noble gases have maximum ionization proxy (equal to period length). -/
  73theorem noble_max_ionization (Z : ℕ) (h : isNobleGas Z) :
  74    ionizationProxy Z = periodLength Z := by
  75  simp only [ionizationProxy]
  76  exact noble_gas_complete_shell Z h
  77
  78/-- Ionization proxy is monotone increasing within a period.
  79    If Z₁ < Z₂ are in the same period, then proxy(Z₁) < proxy(Z₂). -/
  80theorem ionization_monotone_within_period (Z1 Z2 : ℕ)
  81    (hZ1ge : Z1 ≥ prevClosure Z1)
  82    (hLt : Z1 < Z2) (hNotCross : prevClosure Z1 = prevClosure Z2) :
  83    ionizationProxy Z1 < ionizationProxy Z2 := by
  84  simp only [ionizationProxy, valenceElectrons]
  85  -- Z1 - prevClosure Z1 < Z2 - prevClosure Z2
  86  -- Since prevClosure Z1 = prevClosure Z2, this reduces to Z1 < Z2
  87  have hZ2ge : Z2 ≥ prevClosure Z2 := by omega
  88  omega
  89
  90/-! ## Sawtooth Pattern -/
  91
  92/-- The sawtooth pattern: ionization resets at each period boundary.
  93    After a noble gas, the next element (alkali) has minimal ionization. -/
  94theorem sawtooth_reset (Znoble Zalkali : ℕ)
  95    (hNoble : isNobleGas Znoble)
  96    (hNext : Zalkali = Znoble + 1)
  97    (hValid : Zalkali ≤ 118) :
  98    ionizationProxy Zalkali < ionizationProxy Znoble := by
  99  -- Noble gas has maximum (= period length), alkali has 1
 100  -- Case by case on which noble gas
 101  unfold isNobleGas nobleGasZ at hNoble
 102  simp only [List.mem_cons, List.mem_nil_iff, or_false] at hNoble
 103  obtain rfl | rfl | rfl | rfl | rfl | rfl := hNoble <;>
 104    subst hNext <;>
 105    native_decide
 106
 107/-! ## Falsification Criteria
 108
 109The ionization energy derivation is falsifiable:
 110
 1111. **Ordering violation**: If any element Z₁ < Z₂ within the same period
 112   has I₁(Z₁) > I₁(Z₂) in NIST data (beyond experimental error).
 113
 1142. **Alkali not minimum**: If any alkali metal does NOT have minimum I₁
 115   in its period (excluding period 1).
 116
 1173. **Noble not maximum**: If any noble gas does NOT have maximum I₁
 118   in its period.
 119
 1204. **Sawtooth failure**: If I₁(alkali) > I₁(previous noble gas).
 121
 122Note: The NUMERICAL values are not predicted without an anchor.
 123Only the ORDERING is fit-free.
 124-/
 125
 126end
 127end IonizationEnergy
 128end Chemistry
 129end IndisputableMonolith
 130