d_subshell_capacity
plain-language theorem explainer
The theorem states that the d-subshell with angular momentum l=2 accommodates exactly 10 electron states. Quantum chemists constructing electron configurations for transition metals would cite this when filling 3d orbitals. The proof reduces directly to the definition of subshell capacity via a reflexivity step.
Claim. The number of states in a subshell with angular momentum $l=2$ equals $10$, i.e., $2(2l+1)=10$.
background
In Recognition Science the Pauli exclusion principle follows from ledger single-occupancy: fermions carry an odd phase through the eight-tick cycle, so two identical entries at the same address would violate antisymmetry and force the wavefunction to zero. The module therefore derives atomic shell structure from this constraint. The supporting definition states that the number of states in a subshell with angular momentum l is given by subshellCapacity(l) := 2*(2*l + 1), where the leading factor of 2 accounts for spin.
proof idea
The proof is a one-line term that applies reflexivity to the definition of subshellCapacity at argument 2, which evaluates directly to 10.
why it matters
This declaration supplies the concrete capacity for the d-subshell (l=2) inside the derivation of atomic shell structure from ledger single-occupancy. It sits downstream of the general subshellCapacity definition and supports the module's target of obtaining the periodic table and degeneracy pressure from Recognition Science axioms. The result aligns with the eight-tick octave and the odd-phase property of fermions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.