pith. machine review for the scientific record. sign in
def definition def or abbrev high

prevClosure

show as:
view Lean formalization →

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.

claimFor 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 in Recognition Science

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.

scope and limits

formal statement (Lean)

 126def prevClosure (Z : ℕ) : ℕ :=

proof body

Definition body.

 127  if Z ≤ 2 then 0
 128  else if Z ≤ 10 then 2
 129  else if Z ≤ 18 then 10
 130  else if Z ≤ 36 then 18
 131  else if Z ≤ 54 then 36
 132  else if Z ≤ 86 then 54
 133  else 86
 134
 135/-- Next noble gas closure for element Z. -/

used by (20)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (3)

Lean names referenced from this declaration's body.