nextClosure
plain-language theorem explainer
NextClosure maps each atomic number Z to the atomic number of the next noble gas closure. Recognition Science chemists cite it to derive period trends in radii and affinities from the eight-tick neutrality rule. The definition implements this via a chain of threshold comparisons against the sequence 2, 10, 18, 36, 54, 86, 118.
Claim. Let $n(Z)$ be the next noble gas closure for atomic number $Z$. Then $n(Z) = 2$ when $Z ≤ 2$, $n(Z) = 10$ when $Z ≤ 10$, $n(Z) = 18$ when $Z ≤ 18$, $n(Z) = 36$ when $Z ≤ 36$, $n(Z) = 54$ when $Z ≤ 54$, $n(Z) = 86$ when $Z ≤ 86$, and $n(Z) = 118$ otherwise.
background
The PeriodicTable module supplies a zero-parameter scaffold that maps the eight-tick octave to chemical shell closures through phi-tier rails and fixed s/p/d/f block offsets. Noble gases are defined exactly as the points where cumulative valence cost satisfies 8-window neutrality. The module states: 'noble gases are exactly those elements where the cumulative valence cost achieves 8-window neutrality. This is the chemical manifestation of the 8-tick ledger balance.'
proof idea
The definition is built by successive conditional checks. It returns 2 for Z ≤ 2, 10 for Z ≤ 10, 18 for Z ≤ 18, 36 for Z ≤ 36, 54 for Z ≤ 54, 86 for Z ≤ 86, and 118 otherwise. No external lemmas are invoked.
why it matters
This definition realizes the Noble Gas Closure Theorem (P0-A0) from the module documentation. It is invoked by normalizedRadius and lower_z_more_remaining in AtomicRadii plus ea_decreases_within_period and halogen_max_ea in ElectronAffinity. It encodes the chemical form of the eight-tick ledger balance and supplies the deterministic period boundaries required by the Recognition framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.