shell_filling_pattern
plain-language theorem explainer
Shell filling follows the 2n² pattern, with the first two shells summing to 10 electrons and the first three to 28. Atomic and condensed-matter physicists deriving the periodic table from ledger constraints would cite this verification. The proof is a one-line term wrapper that splits the conjunction and applies reflexivity to the arithmetic.
Claim. Let $C(n) = 2n^2$ be the electron capacity of shell $n$. Then $C(1) + C(2) = 10$ and $C(1) + C(2) + C(3) = 28$.
background
The QFT-004 module derives the Pauli exclusion principle from ledger single-occupancy: fermions carry odd phase through the 8-tick cycle, forcing antisymmetry so that identical entries at the same address cancel and yield zero amplitude. This single-occupancy rule produces atomic shell structure and the periodic table. The upstream shellCapacity definition in PeriodicTableFromPhiLadder sets $C(n) := 2n^2$, while the sibling definition in PeriodicTable lists the explicit sequence beginning at n=0; both are invoked to confirm the cumulative counts.
proof idea
The proof is a one-line wrapper that applies constructor to split the conjunction, then reflexivity to verify both equalities hold directly under the shellCapacity definition.
why it matters
The result confirms that the 2n² pattern required by the phi-ladder matches the cumulative capacities needed for the periodic table. It fills the module target of a PRB paper deriving atomic shell structure from first principles via ledger constraints. The theorem sits inside the chain from T7 eight-tick octave and single-occupancy to degeneracy pressure in white dwarfs and neutron stars; no downstream uses are recorded yet.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.