distToNextClosure

formal source

 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
 157/-- Signed valence cost: measures "ledger imbalance" within a period.
 158    Runs from +1 (alkali) through 0 (halfway) to +periodLen (noble gas).
 159    The sum over a complete period is (1+2+...+n) which is NOT zero.
 160
 161    For 8-window neutrality, we use a different proxy below. -/
 162def signedValenceCost (Z : ℕ) : ℤ :=
 163  let v := valenceElectrons Z
 164  let periodLen := periodLength Z
 165  if 2 * v ≤ periodLen then (v : ℤ) else (v : ℤ) - (periodLen : ℤ)
 166
 167/-- Predicate: Z is a noble gas (shell closure point). -/
 168def isNobleGas (Z : ℕ) : Prop := Z ∈ nobleGasZ
 169
 170/-- Decidable instance for noble gas membership. -/
 171instance : DecidablePred isNobleGas := fun Z =>
 172  if h : Z ∈ nobleGasZ then isTrue h else isFalse h
 173
 174/-! ## Noble Gas Closure Theorems -/
 175
 176/-- Helium (Z=2) is a noble gas. -/
 177theorem helium_is_noble : isNobleGas 2 := by native_decide