  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

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.