helium_electrons
plain-language theorem explainer
Helium's electron count is fixed at 2 as the zeroth entry in the noble gas sequence. Researchers deriving atomic shell structure from Recognition Science ledger constraints would cite this as the base case. The proof reduces immediately by reflexivity to the explicit list definition of noble gas electron counts.
Claim. The electron count for helium satisfies $n = 2$, matching the initial term in the noble gas sequence $[2, 10, 18, 36, 54, 86]$.
background
The module derives the Pauli exclusion principle from ledger single-occupancy: fermions carry odd phase through the 8-tick cycle, enforcing antisymmetry so that identical fermions cannot share a quantum state. This yields atomic shell structure and the periodic table. The nobleGasElectrons definition supplies the cumulative filled-shell counts as the list [2, 10, 18, 36, 54, 86].
proof idea
The proof is a one-line reflexivity wrapper that matches the statement directly to the definition of nobleGasElectrons.
why it matters
This theorem supplies the helium base case for the derivation of atomic shell capacities from ledger single-occupancy. It supports the module target of a first-principles account of the periodic table in a PRB paper. The result sits inside the eight-tick octave structure that produces the odd-phase constraint for fermions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.