neon_electrons
plain-language theorem explainer
Neon receives an electron count of 10 as the second entry in the noble gas sequence generated from Recognition Science ledger single-occupancy. Researchers constructing atomic shell structure directly from the derived Pauli exclusion principle would reference this assignment. The proof reduces to reflexivity on the fixed list definition.
Claim. The second entry of the noble gas electron counts list equals 10, matching the configuration $1s^2 2s^2 2p^6$ for neon.
background
The module derives the Pauli exclusion principle from ledger single-occupancy: fermions carry odd phase through the 8-tick cycle, forcing antisymmetry that prohibits two identical entries in one state. The definition nobleGasElectrons supplies the cumulative filled-shell counts [2, 10, 18, 36, 54, 86] for helium through radon. This theorem simply confirms the neon position in that sequence.
proof idea
One-line wrapper applying reflexivity to the definition of nobleGasElectrons.
why it matters
The result populates the electron count sequence that follows from the ledger-derived Pauli principle and supports the module's target of first-principles atomic shell structure. It connects the odd-phase fermion constraint and 8-tick cycle directly to the periodic table entries. No downstream uses are recorded yet.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.