f_subshell_capacity
plain-language theorem explainer
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.
Claim. The 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
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.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.