`nextClosure`

definition

show as: view math explainer →

module: IndisputableMonolith.Chemistry.PeriodicTable
domain: Chemistry
line: 136 · github
papers citing: none yet

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.Chemistry.PeriodicTable on GitHub at line 136.

browse module

All declarations in this module, on Recognition.

explainer page

A cached Ask Recognition explainer exists for this declaration.

open explainer

depends on

used by

formal source

 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
 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

papers checked against this theorem

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