subshellCapacity
The definition subshellCapacity(l) returns the number of electron states in a subshell with angular momentum l as 2(2l+1). Atomic physicists and quantum chemists cite it when computing shell fillings and periodic table structure. It is supplied as a direct arithmetic definition that the surrounding theorems instantiate for concrete l values.
claimThe number of quantum states in a subshell with angular momentum quantum number $l$ is $2(2l+1)$, where the leading factor of 2 accounts for spin.
background
The QFT-004 module derives the Pauli exclusion principle from ledger single-occupancy: fermions are odd-phase entries under the eight-tick cycle, so the ledger balance condition forces antisymmetric wavefunctions and therefore zero amplitude for two identical fermions at the same address. The subshellCapacity definition supplies the combinatorial count of distinct states once the orbital angular momentum quantum number $l$ is given. The module imports SpinStatistics to link half-integer spin to the required antisymmetry.
proof idea
This is a direct definition that unfolds to the arithmetic expression 2*(2*l + 1). The surrounding theorems apply reflexivity to obtain the concrete values 2, 6, 10, 14 for l = 0, 1, 2, 3.
why it matters in Recognition Science
This definition supplies the numerical capacities that appear in the PauliProofSummary structure, which collects the full chain from antisymmetry to shell capacities 2, 6, 10, 14 and onward to degeneracy pressure and the Chandrasekhar limit. It fills the combinatorial step in the paper proposition deriving atomic shell structure from Recognition Science ledger rules. The eight-tick cycle and odd-phase fermions underwrite the spin factor of 2.
scope and limits
- Does not derive the spin degeneracy factor from ledger rules.
- Does not connect the formula to explicit ledger address structure.
- Does not address relativistic corrections or fine structure splitting.
formal statement (Lean)
85def subshellCapacity (l : ℕ) : ℕ := 2 * (2 * l + 1)
proof body
Definition body.
86
87/-- **THEOREM**: s-subshell (l=0) holds 2 electrons. -/