shell_sum_to_noble
plain-language theorem explainer
The mapped cumulative shell closures over indices 0 to 5 equal the noble gas atomic numbers [2, 10, 18, 36, 54, 86]. Chemists using Recognition Science's ledger model would cite this to anchor the forced periodic closures. The proof is a one-line native_decide that evaluates the concrete list equality.
Claim. The list obtained by applying the cumulative shell closure function to each integer from 0 to 5 equals the list of noble gas atomic numbers $[2, 10, 18, 36, 54, 86]$.
background
In the Periodic Table Engine the cumulativeShellClosure function returns the cumulative electron count at shell closure n, defined to produce the noble gas atomic numbers. The nobleGasZ definition supplies the target list [2, 10, 18, 36, 54, 86]. The module states that noble gases are exactly the elements where cumulative valence cost achieves 8-window neutrality, the chemical form of the 8-tick ledger balance.
proof idea
The proof is a one-line wrapper that applies native_decide to confirm the equality by direct evaluation of both sides on the concrete values.
why it matters
This theorem supports the Noble Gas Closure Theorem (P0-A0) by verifying that the set {2, 10, 18, 36, 54, 86} is forced by 8-window neutrality under the deterministic valence proxy. It instantiates the eight-tick octave (T7) inside the chemistry domain. No downstream uses appear yet, so its role in later mass-ladder or alpha-band arguments remains open.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.