prevClosure
plain-language theorem explainer
The previous noble gas closure function maps each atomic number Z to the closure number of the preceding noble gas in the sequence 0, 2, 10, 18, 36, 54, 86. Researchers deriving intra-period radii or electronegativity rankings inside the Recognition Science model cite it as the lower bound for normalization. The implementation is a direct piecewise constant function on fixed intervals with no external lemmas.
Claim. For natural number $Z$, the previous noble-gas closure $p(Z)$ equals 0 if $Zleq 2$, 2 if $3leq Zleq 10$, 10 if $11leq Zleq 18$, 18 if $19leq Zleq 36$, 36 if $37leq Zleq 54$, 54 if $55leq Zleq 86$, and 86 otherwise.
background
The Periodic Table Engine maps the eight-tick octave onto chemistry via phi-tier rails and a fixed set of block offsets. Noble gases arise exactly where cumulative valence cost meets 8-window neutrality, producing the deterministic closure sequence 2, 10, 18, 36, 54, 86. This encodes the 8-tick ledger balance as the chemical manifestation of the fundamental RS scheduler.
proof idea
The definition executes successive interval tests against the thresholds 2, 10, 18, 36, 54 and 86, returning the prior closure value in each case. No lemmas from the upstream forcing or anchor modules are applied; the body is a pure conditional expression.
why it matters
This supplies the lower endpoint for the normalized radius definition and for the electronegativity ranking theorems such as chlorine greater than sodium and carbon intermediate. It realizes the Noble Gas Closure Theorem (P0-A0) by embedding the eight-tick neutrality condition directly into the periodic table. The construction aligns with T7 of the unified forcing chain and supports twenty downstream results on atomic trends.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.