d_subshell_capacity
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.
claimThe 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 in Recognition Science
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.
scope and limits
- Does not derive the 2(2l+1) formula from ledger axioms.
- Does not include relativistic corrections or spin-orbit coupling.
- Does not treat multi-electron interactions beyond single-occupancy.
formal statement (Lean)
94theorem d_subshell_capacity : subshellCapacity 2 = 10 := rfl
proof body
Term-mode proof.
95
96/-- **THEOREM**: f-subshell (l=3) holds 14 electrons. -/