f_subshell_capacity
The declaration states that the f-subshell with angular momentum l=3 holds exactly 14 electrons. Quantum chemists constructing electron configurations for f-block elements would cite this when enumerating orbital occupancies. The proof reduces immediately to reflexivity on the closed-form subshell capacity expression.
claimThe number of states in a subshell with angular momentum $l=3$ equals 14, i.e., $2(2l+1)=14$.
background
Subshell capacity counts the available quantum states for a given orbital angular momentum l. The upstream definition supplies the formula subshellCapacity(l) := 2*(2*l + 1), where the factor 2 accounts for spin and 2l+1 for the magnetic quantum numbers m_l. This module derives the Pauli exclusion principle from Recognition Science ledger single-occupancy: fermions carry an odd phase through the eight-tick cycle, enforcing antisymmetry that forbids two identical entries in the same ledger slot and thereby produces atomic shell structure.
proof idea
The proof is a one-line term that applies reflexivity directly to the definition of subshellCapacity evaluated at l=3.
why it matters in Recognition Science
This instance populates the subshell sequence 2, 6, 10, 14 that generates the periodic table. It follows from the ledger-derived Pauli exclusion principle stated in the module documentation, which links single-occupancy to degeneracy pressure and matter stability. The result sits inside the QFT-004 target of first-principles shell structure.
scope and limits
- Does not derive the general subshellCapacity formula from ledger axioms.
- Does not include relativistic corrections or spin-orbit coupling.
- Does not compute full shell capacities or periodic-table filling order.
formal statement (Lean)
97theorem f_subshell_capacity : subshellCapacity 3 = 14 := rfl
proof body
Term-mode proof.
98
99/-- **THEOREM**: Subshell capacities form the sequence 2, 6, 10, 14, ... -/