`d_subshell_capacity`

proved

show as: view math explainer →

module: IndisputableMonolith.QFT.PauliExclusion
domain: QFT
line: 94 · github
papers citing: none yet

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.QFT.PauliExclusion on GitHub at line 94.

browse module

All declarations in this module, on Recognition.

explainer page

A cached Ask Recognition explainer exists for this declaration.

open explainer

depends on

subshellCapacity IndisputableMonolith.QFT.PauliExclusion

formal source

  91theorem p_subshell_capacity : subshellCapacity 1 = 6 := rfl
  92
  93/-- **THEOREM**: d-subshell (l=2) holds 10 electrons. -/
  94theorem d_subshell_capacity : subshellCapacity 2 = 10 := rfl
  95
  96/-- **THEOREM**: f-subshell (l=3) holds 14 electrons. -/
  97theorem f_subshell_capacity : subshellCapacity 3 = 14 := rfl
  98
  99/-- **THEOREM**: Subshell capacities form the sequence 2, 6, 10, 14, ... -/
 100theorem subshell_capacity_formula (l : ℕ) :
 101    subshellCapacity l = 4 * l + 2 := by
 102  unfold subshellCapacity; ring
 103
 104/-- Number of states in a shell with principal quantum number n.
 105    Formula: 2n² -/
 106def shellCapacity (n : ℕ) : ℕ := 2 * n^2
 107
 108/-- **THEOREM**: First shell (n=1) holds 2 electrons. -/
 109theorem first_shell_capacity : shellCapacity 1 = 2 := rfl
 110
 111/-- **THEOREM**: Second shell (n=2) holds 8 electrons. -/
 112theorem second_shell_capacity : shellCapacity 2 = 8 := rfl
 113
 114/-- **THEOREM**: Third shell (n=3) holds 18 electrons. -/
 115theorem third_shell_capacity : shellCapacity 3 = 18 := rfl
 116
 117/-- **THEOREM**: Fourth shell (n=4) holds 32 electrons. -/
 118theorem fourth_shell_capacity : shellCapacity 4 = 32 := rfl
 119
 120/-! ## Noble Gas Configurations -/
 121
 122/-- Noble gas electron counts (cumulative filled shells). -/
 123def nobleGasElectrons : List ℕ := [2, 10, 18, 36, 54, 86]
 124

papers checked against this theorem

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