second_shell_capacity
plain-language theorem explainer
The second shell capacity theorem states that the n=2 electron shell accommodates exactly eight electrons. Chemists and quantum theorists working from Recognition Science ledger constraints would cite this when constructing the periodic table sequence. The proof is a one-line reflexivity reduction on the shellCapacity definition.
Claim. The number of states in the shell with principal quantum number 2 satisfies $2n^2 = 8$ at $n=2$.
background
The QFT.PauliExclusion module derives the Pauli exclusion principle from ledger single-occupancy for fermions carrying odd phase through the eight-tick cycle. This forces antisymmetry and therefore single occupancy per quantum state, which directly yields atomic shell capacities. The local shellCapacity definition is shellCapacity (n : ℕ) := 2 * n^2. Upstream, PeriodicTableFromPhiLadder supplies the same 2n² formula while PeriodicTable lists the explicit sequence beginning 2, 8, 8, 18, … and PeriodicBlocks scales shell energies by E_coh times capacity.
proof idea
This is a one-line term proof that applies reflexivity to the shellCapacity definition evaluated at n=2, which reduces algebraically to 8.
why it matters
The result instantiates the general shellCapacity formula for the second shell and feeds the derivation of periodic table structure from Recognition Science. It supports the PRB paper proposition on first-principles derivation of atomic shell structure. The theorem closes one concrete case in the ledger-to-shell chain that begins from the eight-tick octave and single-occupancy constraint.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.