`subshellCapacity`

definition

show as: view math explainer →

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

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.QFT.PauliExclusion on GitHub at line 85.

browse module

All declarations in this module, on Recognition.

explainer page

A cached Ask Recognition explainer exists for this declaration.

open explainer

used by

formal source

  82
  83/-- Number of states in a subshell with angular momentum l.
  84    Formula: 2(2l+1) where factor 2 is for spin. -/
  85def subshellCapacity (l : ℕ) : ℕ := 2 * (2 * l + 1)
  86
  87/-- **THEOREM**: s-subshell (l=0) holds 2 electrons. -/
  88theorem s_subshell_capacity : subshellCapacity 0 = 2 := rfl
  89
  90/-- **THEOREM**: p-subshell (l=1) holds 6 electrons. -/
  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

papers checked against this theorem

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