shellCapacity
plain-language theorem explainer
Electron shell capacity for principal quantum number n equals 2n squared. Researchers reconstructing the periodic table from Recognition Science ledger constraints cite this when verifying block occupancies. The definition is a direct encoding of the standard formula also appearing in the Pauli exclusion module.
Claim. The maximum number of electrons in the shell with principal quantum number $n$ is $2n^2$.
background
The module derives periodic table structure from the phi-ladder while noting that shell capacities follow the standard 2n² sequence rather than direct phi powers. Electron blocks total five types (s, p, d, f, g), matching configDim D = 5. Upstream, the Pauli exclusion result defines the same capacity as the number of states in a shell with principal quantum number n, while the PeriodicTable module gives an explicit sequence for periods. The module states that capacities are 2, 8, 18, 32 = 2n² for n = 1, 2, 3, 4, and that these are not phi-ladder but the number of periodic table blocks totals 32 = 2^5.
proof idea
This declaration is a one-line definition that directly sets shell capacity to twice the square of the input natural number.
why it matters
It supplies the capacity values required by PeriodicTableCert to certify five blocks with capacities 2, 8, 18, 32 for the first four shells. This anchors the standard quantum result inside the Recognition Science framework, where angular momentum quantization arises from ledger packing. The definition supports the separation between shell capacities (2n²) and the phi-ladder pattern for period lengths.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.