s_subshell_capacity
plain-language theorem explainer
The declaration establishes that the s-subshell with angular momentum l=0 accommodates exactly two electrons under the standard capacity formula. Atomic physicists building electron configurations from ledger-based derivations would cite this when populating shell summaries. The proof is a direct reflexivity reduction on the subshell capacity definition evaluated at zero.
Claim. The number of states in the subshell with orbital angular momentum $l=0$ is $2$, where capacity is defined by the formula $2(2l+1)$.
background
The QFT.PauliExclusion module derives the Pauli exclusion principle from Recognition Science ledger single-occupancy. Fermions correspond to odd-phase entries that accumulate a minus sign over the eight-tick cycle, enforcing antisymmetry and therefore zero amplitude for two identical particles in one state. The upstream subshellCapacity definition supplies the counting rule: number of states in a subshell with angular momentum l equals 2 times (2l + 1), with the leading factor of two arising from spin degeneracy.
proof idea
The proof is a one-line term-mode wrapper that applies reflexivity directly to the subshellCapacity definition at input 0, which computes as 2 * (2 * 0 + 1) = 2.
why it matters
This theorem supplies the s_shell entry inside the pauliProofs summary that assembles the full ledger-based argument for exclusion. It fills the concrete shell-capacity step in the PRB paper proposition on first-principles atomic structure. The result instantiates the consequences of the eight-tick octave and single-occupancy constraint for three spatial dimensions, directly supporting the observed periodic table organization.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.