periodLength
plain-language theorem explainer
The definition computes the length of the chemical period containing atomic number Z as the difference between the next and previous noble-gas closure points. Atomic-radius and shell-closure calculations in the Recognition framework cite it to verify complete shells without empirical tuning. The implementation is a direct one-line subtraction of the two closure functions already defined in the same module.
Claim. For atomic number $Z$, the period length is defined by $l(Z) := C_+(Z) - C_-(Z)$, where $C_+(Z)$ is the smallest noble-gas closure at or above $Z$ and $C_-(Z)$ is the largest noble-gas closure strictly below $Z$.
background
The Periodic Table Engine treats chemistry as an eight-tick octave realized on φ-tier rails with fixed s/p/d/f block offsets and an eight-window neutrality predicate. Noble gases are defined exactly as the points where cumulative valence cost returns to neutrality, implementing the Noble Gas Closure Theorem (P0-A0) stated in the module documentation: noble gases are exactly those elements where the cumulative valence cost achieves 8-window neutrality.
proof idea
One-line definition that subtracts the value of prevClosure Z from nextClosure Z.
why it matters
It supplies the period length required by the AtomicRadii theorems (helium_full_shell, neon_full_shell, argon_full_shell, krypton_full_shell, radon_full_shell, oganesson_full_shell) that confirm valenceElectrons Z equals periodLength Z at each forced closure. The construction realizes the eight-tick neutrality condition of the RS scheduler as the chemical ledger balance, feeding the downstream claim that the set {2,10,18,36,54,86} is forced by 8-window neutrality with zero free parameters.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.