cumulativeShellClosure
plain-language theorem explainer
The definition supplies the cumulative electron counts at successive shell closures, giving the noble gas atomic numbers 2, 10, 18, 36, 54, 86 and continuing with steps of 32. Researchers applying the eight-tick neutrality condition from Recognition Science to the periodic table would cite this when anchoring chemical periodicity. It is implemented via direct case analysis on the shell index.
Claim. Define the function $c : ℕ → ℕ$ by $c(0) = 2$, $c(1) = 10$, $c(2) = 18$, $c(3) = 36$, $c(4) = 54$, $c(5) = 86$, and $c(n + 6) = 86 + (n + 1) ⋅ 32$ for $n ≥ 0$. The values are the atomic numbers of the noble gases.
background
The Periodic Table Engine realizes an octave-to-eight-tick mapping for chemistry through φ-tier rails with fixed block offsets for the s, p, d, and f subshells. Closures are identified by an eight-window neutrality predicate on cumulative valence cost, which manifests the 8-tick ledger balance. The module states that noble gases are exactly the elements where this cumulative cost achieves 8-window neutrality and that the set {2, 10, 18, 36, 54, 86} is forced by the requirement of shell closures at these neutrality points. Upstream results on J-cost convexity from PhiForcingDerived and ledger factorization from DAlembert provide the underlying minimization principle.
proof idea
The definition is given explicitly by pattern matching on the natural-number argument, returning the six initial noble-gas numbers and applying the linear continuation formula for all larger arguments.
why it matters
This definition provides the numerical sequence required by the Noble Gas Closure Theorem in the module documentation. It is used by the theorem verifying that cumulative closures match the noble gas sequence exactly and by the theorem showing that shell capacities sum to the noble gas atomic numbers. Within the Recognition Science framework it instantiates the T7 eight-tick octave as the source of chemical periodicity, completing the step from the forcing chain to element structure without free parameters.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.