distToNextClosure
plain-language theorem explainer
The definition computes the number of elements from atomic number Z until the next noble gas closure. Chemists deriving periodic radius trends and electron affinity patterns cite it for within-period contraction arguments. It is realized as a direct subtraction from the precomputed next noble gas locator.
Claim. For atomic number $Z$, the distance to the next noble gas closure equals the atomic number of the smallest noble gas at or above $Z$, minus $Z$.
background
The Periodic Table Engine implements an eight-tick octave mapping for chemistry through phi-tier rails and a fixed set of block offsets. Noble gas closures are defined exactly as the points where cumulative valence cost satisfies 8-window neutrality, the chemical counterpart of the ledger balance condition. The nextClosure locator supplies the fixed sequence of these points as 2, 10, 18, 36, 54 and onward.
proof idea
This definition is a one-line wrapper that subtracts the input atomic number from the result of the nextClosure locator.
why it matters
It supplies the distance metric used by the radius contraction theorem lower_z_more_remaining and the halogen checks at_dist_one through i_dist_one in AtomicRadii. The declaration operationalizes the Noble Gas Closure Theorem (P0-A0) stated in the module, linking directly to the eight-tick neutrality of the fundamental scheduler. It supports downstream falsifiable predictions for electron affinity decrease within periods.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.