subshell_capacity_formula
plain-language theorem explainer
Subshell capacities equal 4l + 2 for angular momentum quantum number l, producing the sequence 2, 6, 10, 14. Atomic physicists and chemists working from Recognition Science ledger single-occupancy would cite this identity to obtain standard shell degeneracies. The proof is a one-line term that unfolds the subshellCapacity definition and applies the ring tactic.
Claim. For each natural number $l$, the number of states in the subshell with orbital angular momentum $l$ equals $4l + 2$.
background
The QFT.PauliExclusion module derives the Pauli exclusion principle from ledger single-occupancy: fermions are odd-phase ledger entries that accumulate a minus sign over the eight-tick cycle, forcing antisymmetry so that identical states cannot be doubly occupied. The subshellCapacity function counts the available states for given $l$, incorporating the two spin orientations that survive the antisymmetry constraint. Upstream, SpectralEmergence.of supplies the 24 chiral fermion flavors (= $D × 2^D = 3 × 8$) that set the total fermionic degrees of freedom, while PhiForcingDerived.of encodes the convex J-cost minimization that selects the stable occupancy pattern.
proof idea
This is a one-line wrapper proof. It unfolds the definition of subshellCapacity and applies the ring tactic to verify the algebraic identity.
why it matters
The theorem supplies the explicit degeneracy factors that realize atomic shell structure from the ledger-derived Pauli principle. It supports the paper proposition on first-principles derivation of atomic shell structure and connects to the eight-tick octave (T7) together with the emergence of three spatial dimensions (T8). No downstream uses are recorded yet, so the result currently functions as a terminal identity in the QFT layer.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.