IndisputableMonolith.Chemistry.AtomicRadii

   1import Mathlib
   2import IndisputableMonolith.Constants
   3import IndisputableMonolith.Chemistry.PeriodicTable
   4
   5/-!
   6# Atomic Radii from φ-Ladder Scaling (CH-007)
   7
   8RS predicts atomic radii follow shell structure:
   9
  101. **Period trend**: Radii DECREASE across a period (increasing Z pulls electrons closer)
  112. **Group trend**: Radii INCREASE down a group (new shells are farther from nucleus)
  123. **Lanthanide/actinide contraction**: d/f-block filling causes radius contraction
  13
  14**RS Mechanism**: Radii scale with coherence length and shell number.
  15- Base radius ~ φ^n where n is the shell number
  16- Effective radius decreases with valence electrons (screening penetration)
  17
  18**Key predictions**:
  19- Noble gases have LOCAL maxima in their periods (but special due to closed shell)
  20- Alkali metals have MAXIMA after noble gas (new shell starts)
  21- Halogens approach minimum before closure
  22-/
  23
  24namespace IndisputableMonolith
  25namespace Chemistry
  26namespace AtomicRadii
  27
  28open PeriodicTable
  29
  30noncomputable section
  31
  32/-- Shell number (1-indexed) for atomic radii scaling. -/
  33def shellNumber (Z : ℕ) : ℕ := periodOf Z + 1
  34
  35/-- Raw shell radius proxy: φ^(shell_number).
  36    Higher shell = larger base radius. -/
  37def shellRadiusProxy (Z : ℕ) : ℝ :=
  38  Constants.phi ^ (shellNumber Z : ℝ)
  39
  40/-- Screening factor: valence electrons penetrate less as they increase.
  41    radius ~ shellRadius * (1 - valence/periodLength) -/
  42def screeningFactor (Z : ℕ) : ℝ :=
  43  if periodLength Z = 0 then 1
  44  else 1 - (valenceElectrons Z : ℝ) / (2 * periodLength Z : ℝ)
  45
  46/-- Atomic radius proxy: combines shell and screening effects.
  47    radius = shellRadius * screeningFactor -/
  48def radiusProxy (Z : ℕ) : ℝ :=
  49  shellRadiusProxy Z * screeningFactor Z
  50
  51/-- Normalized atomic radius (0 to 1 within period).
  52    0 = smallest in period, 1 = largest. -/
  53def normalizedRadius (Z : ℕ) : ℝ :=
  54  let prev := prevClosure Z
  55  let next := nextClosure Z
  56  if next = prev then 1
  57  else 1 - (Z - prev : ℝ) / (next - prev : ℝ)
  58
  59/-! ## Period Trends -/
  60
  61/-- Within a period, lower Z has more "remaining capacity" to next closure.
  62    This is the basic principle of across-period radius contraction. -/
  63theorem lower_z_more_remaining (Z1 Z2 : ℕ) (hLt : Z1 < Z2)
  64    (hZ1_le : Z1 ≤ nextClosure Z1)
  65    (hZ2_le : Z2 ≤ nextClosure Z2)
  66    (hSameNext : nextClosure Z1 = nextClosure Z2) :
  67    distToNextClosure Z1 > distToNextClosure Z2 := by
  68  simp only [distToNextClosure]
  69  omega
  70
  71/-! ## Group Trends -/
  72
  73/-- Shell radius increases with period number.
  74    Period 2 elements are smaller than Period 3 counterparts. -/
  75theorem shell_radius_increases_with_period (n m : ℕ)
  76    (hLt : n < m) :
  77    Constants.phi ^ (n : ℝ) < Constants.phi ^ (m : ℝ) := by
  78  have hphi_gt_1 : (1 : ℝ) < Constants.phi := by
  79    have h := Constants.phi_gt_onePointFive
  80    linarith
  81  apply Real.rpow_lt_rpow_of_exponent_lt hphi_gt_1
  82  exact Nat.cast_lt.mpr hLt
  83
  84/-! ## Specific Element Theorems -/
  85
  86/-- Alkali metals start new shells, so have valence = 1. -/
  87theorem li_valence_one : valenceElectrons 3 = 1 := by native_decide
  88theorem na_valence_one : valenceElectrons 11 = 1 := by native_decide
  89theorem k_valence_one : valenceElectrons 19 = 1 := by native_decide
  90theorem rb_valence_one : valenceElectrons 37 = 1 := by native_decide
  91theorem cs_valence_one : valenceElectrons 55 = 1 := by native_decide
  92theorem fr_valence_one : valenceElectrons 87 = 1 := by native_decide
  93
  94/-- Halogens are one from closure, near minimum radius for their period. -/
  95theorem f_dist_one : distToNextClosure 9 = 1 := by native_decide
  96theorem cl_dist_one : distToNextClosure 17 = 1 := by native_decide
  97theorem br_dist_one : distToNextClosure 35 = 1 := by native_decide
  98theorem i_dist_one : distToNextClosure 53 = 1 := by native_decide
  99theorem at_dist_one : distToNextClosure 85 = 1 := by native_decide
 100
 101/-- Noble gases have complete shells: valenceElectrons = periodLength. -/
 102theorem helium_full_shell : valenceElectrons 2 = periodLength 2 := by native_decide
 103theorem neon_full_shell : valenceElectrons 10 = periodLength 10 := by native_decide
 104theorem argon_full_shell : valenceElectrons 18 = periodLength 18 := by native_decide
 105theorem krypton_full_shell : valenceElectrons 36 = periodLength 36 := by native_decide
 106theorem xenon_full_shell : valenceElectrons 54 = periodLength 54 := by native_decide
 107theorem radon_full_shell : valenceElectrons 86 = periodLength 86 := by native_decide
 108theorem oganesson_full_shell : valenceElectrons 118 = periodLength 118 := by native_decide
 109
 110/-! ## Ordering Lemmas -/
 111
 112/-- Li (Z=3) has larger radius than F (Z=9) in Period 2.
 113    Li: (1 - (3-2)/(10-2)) = 7/8
 114    F:  (1 - (9-2)/(10-2)) = 1/8 -/
 115theorem li_larger_than_f : normalizedRadius 3 > normalizedRadius 9 := by
 116  simp only [normalizedRadius, prevClosure, nextClosure]
 117  norm_num
 118
 119/-- Na (Z=11) has larger radius than Cl (Z=17) in Period 3.
 120    Na: (1 - (11-10)/(18-10)) = 7/8
 121    Cl: (1 - (17-10)/(18-10)) = 1/8 -/
 122theorem na_larger_than_cl : normalizedRadius 11 > normalizedRadius 17 := by
 123  simp only [normalizedRadius, prevClosure, nextClosure]
 124  norm_num
 125
 126/-- K (Z=19) has larger shell number than Li (Z=3) due to more shells. -/
 127theorem k_larger_shell_than_li : shellNumber 19 > shellNumber 3 := by
 128  native_decide
 129
 130/-! ## Falsification Criteria
 131
 132The atomic radii derivation is falsifiable:
 133
 1341. **Period trend violation**: If radius increases across a period (same shell).
 135
 1362. **Group trend violation**: If radius decreases going down a group.
 137
 1383. **Alkali not maximum**: If alkali metal does NOT have maximum radius in period.
 139
 140Note: Actual radii in pm are NOT predicted without a scale anchor.
 141Only the ORDERING and TRENDS are fit-free predictions.
 142-/
 143
 144end
 145end AtomicRadii
 146end Chemistry
 147end IndisputableMonolith
 148