p_subshell_capacity
plain-language theorem explainer
The theorem asserts that the p-subshell with angular momentum l=1 accommodates exactly six electrons. Atomic physicists building electron configurations from Recognition Science ledger rules would cite this when tabulating shell fillings. The proof reduces directly to reflexivity on the subshell capacity definition.
Claim. The p-subshell capacity for angular momentum quantum number $l=1$ equals six electrons, i.e., $2(2l+1)=6$.
background
The QFT-004 module derives the Pauli exclusion principle from ledger single-occupancy: fermions carry an odd phase through the eight-tick cycle, forcing antisymmetry that prohibits two identical entries in one state slot. The upstream subshellCapacity definition supplies the state count as $2(2l+1)$, with the factor of two arising from spin degeneracy. This theorem specializes that formula at $l=1$ to recover the standard p-subshell occupancy.
proof idea
The proof is a one-line term that applies reflexivity directly to the subshellCapacity definition evaluated at argument 1.
why it matters
This result supplies the p_shell field inside the pauliProofs summary that assembles the full Pauli exclusion argument for atomic shell structure. It fills the paper proposition on first-principles derivation of the periodic table from Recognition Science ledger constraints. The specialization is consistent with the eight-tick octave and single-occupancy rule that underpins the framework's spatial dimension count.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.