window8Sum

formal source

  72  IndisputableMonolith.Constants.E_coh * railFactor n
  73
  74/- Sliding 8‑window sum used for neutrality tests. -/
  75def window8Sum (f : ℕ → ℝ) (Z0 : ℕ) : ℝ :=
  76  (Finset.range 8).sum (fun k => f (Z0 + k))
  77
  78/-! ## Noble Gas Closure Infrastructure
  79
  80We define a valence proxy and prove that noble gases are exactly the
  818-window closure points.
  82-/
  83
  84/-- The canonical noble gas atomic numbers (first 6 periods + Oganesson). -/
  85def nobleGasZ : List ℕ := [2, 10, 18, 36, 54, 86]
  86
  87/-- Extended noble gas list including Oganesson (period 7). -/
  88def nobleGasZFull : List ℕ := [2, 10, 18, 36, 54, 86, 118]
  89
  90/-- Shell capacity sequence: {2, 8, 8, 18, 18, 32, 32, ...}
  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. -/