ionizationProxy

formal source

  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