prevClosure

formal source

 123  else 7
 124
 125/-- Previous noble gas closure for element Z. -/
 126def prevClosure (Z : ℕ) : ℕ :=
 127  if Z ≤ 2 then 0
 128  else if Z ≤ 10 then 2
 129  else if Z ≤ 18 then 10
 130  else if Z ≤ 36 then 18
 131  else if Z ≤ 54 then 36
 132  else if Z ≤ 86 then 54
 133  else 86
 134
 135/-- Next noble gas closure for element Z. -/
 136def nextClosure (Z : ℕ) : ℕ :=
 137  if Z ≤ 2 then 2
 138  else if Z ≤ 10 then 10
 139  else if Z ≤ 18 then 18
 140  else if Z ≤ 36 then 36
 141  else if Z ≤ 54 then 54
 142  else if Z ≤ 86 then 86
 143  else 118  -- Oganesson
 144
 145/-- Distance to next noble gas closure.
 146    At noble gases, this equals 0 (shell complete). -/
 147def distToNextClosure (Z : ℕ) : ℕ := nextClosure Z - Z
 148
 149/-- Valence electrons: electrons beyond the previous noble gas core.
 150    At noble gases, this equals the period length (complete shell).
 151    The RS insight: noble gases are exactly those where valence = period length. -/
 152def valenceElectrons (Z : ℕ) : ℕ := Z - prevClosure Z
 153
 154/-- Period length for element Z. -/
 155def periodLength (Z : ℕ) : ℕ := nextClosure Z - prevClosure Z
 156