shellCapacity

formal source

  91    Period n has capacity 2n² electrons, but fills in two sub-periods.
  92    This is the deterministic sequence forced by angular momentum quantization
  93    (which RS derives from ledger packing constraints). -/
  94def shellCapacity : ℕ → ℕ
  95  | 0 => 2       -- 1s²
  96  | 1 => 8       -- 2s² 2p⁶
  97  | 2 => 8       -- 3s² 3p⁶
  98  | 3 => 18      -- 4s² 3d¹⁰ 4p⁶
  99  | 4 => 18      -- 5s² 4d¹⁰ 5p⁶
 100  | 5 => 32      -- 6s² 4f¹⁴ 5d¹⁰ 6p⁶
 101  | 6 => 32      -- 7s² 5f¹⁴ 6d¹⁰ 7p⁶
 102  | _ => 32      -- Continuation pattern
 103
 104/-- Cumulative electron count at shell closure n.
 105    These are exactly the noble gas atomic numbers. -/
 106def cumulativeShellClosure : ℕ → ℕ
 107  | 0 => 2       -- He
 108  | 1 => 10      -- Ne
 109  | 2 => 18      -- Ar
 110  | 3 => 36      -- Kr
 111  | 4 => 54      -- Xe
 112  | 5 => 86      -- Rn
 113  | n + 6 => 86 + (n + 1) * 32  -- Continuation
 114
 115/-- Period of element Z (which noble-gas-bounded period it belongs to). -/
 116def periodOf (Z : ℕ) : ℕ :=
 117  if Z ≤ 2 then 1
 118  else if Z ≤ 10 then 2
 119  else if Z ≤ 18 then 3
 120  else if Z ≤ 36 then 4
 121  else if Z ≤ 54 then 5
 122  else if Z ≤ 86 then 6
 123  else 7
 124