first_shell_capacity
plain-language theorem explainer
Recognition Science derives the first shell capacity as exactly two electrons from the general formula 2n². Quantum chemists building atomic models on ledger single-occupancy would reference this base case when filling the 1s orbital. The equality holds by direct substitution into the definition of shellCapacity.
Claim. The number of states in the shell with principal quantum number $n=1$ equals $2$, where shellCapacity$(n) := 2n^2$.
background
The QFT.PauliExclusion module derives the Pauli exclusion principle from ledger single-occupancy: fermions carry an odd phase through the 8-tick cycle, enforcing antisymmetry so that identical entries at the same address cancel and force zero occupancy. The shellCapacity function is defined locally as 2n², giving the number of states per principal quantum number n. This rests on upstream results: PeriodicTableFromPhiLadder.shellCapacity (n) := 2 * n ^ 2 and the PeriodicTable variant that sequences capacities as {2, 8, 8, 18, ...} from angular-momentum quantization forced by ledger packing.
proof idea
The proof is a one-line term that applies reflexivity on the definition of shellCapacity.
why it matters
This base case anchors the n=1 entry in the shell sequence that feeds the periodic table derivations in PeriodicBlocks and PeriodicTable. It directly supports the paper target of a first-principles derivation of atomic shell structure from Recognition Science ledger constraints and aligns with the T7 eight-tick octave and D=3 spatial dimensions in the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.