shellCapacity
plain-language theorem explainer
The definition assigns to each principal quantum number n the integer value 2n squared as the number of electron states in that shell. Periodic-table constructions and certification structures cite it when verifying the sequence of shell fillings. It is a direct abbreviation of the standard formula with no further reduction required.
Claim. The number of states in a shell with principal quantum number $n$ is $2n^2$.
background
In the QFT-004 module the Pauli exclusion principle is obtained from ledger single-occupancy: fermions carry an odd phase through the 8-tick cycle, so two identical entries at the same address would violate antisymmetry and force the wave function to zero. The shellCapacity definition therefore supplies the counting of available ledger slots per principal quantum number. Upstream, PeriodicTableFromPhiLadder.shellCapacity gives the identical formula 2 * n ^ 2, while PeriodicTable.shellCapacity records the explicit sequence {2, 8, 8, 18, 18, 32, …} forced by angular-momentum quantization derived from ledger packing.
proof idea
This is a direct definition that sets shellCapacity n to 2 * n ^ 2. It matches the explicit formula already present in PeriodicTableFromPhiLadder and is used verbatim by the downstream PeriodicTable module.
why it matters
The definition supplies the capacity formula required by PeriodicTableCert, whose fields include s1_cap : shellCapacity 1 = 2, s2_cap : shellCapacity 2 = 8 and the remaining shell equalities that certify five electron blocks. It therefore fills the paper proposition on first-principles derivation of atomic shell structure from ledger single-occupancy. The result sits inside the Recognition Science chain that obtains D = 3 and the eight-tick octave from the same ledger constraints.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.