def
definition
subshellCapacity
show as:
view math explainer →
open explainer
Generate a durable explainer page for this declaration.
open lean source
IndisputableMonolith.QFT.PauliExclusion on GitHub at line 85.
browse module
All declarations in this module, on Recognition.
explainer page
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