period_lengths_from_noble_gaps
plain-language theorem explainer
Differences between successive noble gas atomic numbers recover the standard period lengths 2, 8, 8, 18, 18, 32. Chemists working inside the Recognition Science scaffold cite this to confirm that eight-window neutrality produces the observed shell closures with no free parameters. The proof is a direct numerical check via native_decide on the listed differences.
Claim. The differences between consecutive noble-gas atomic numbers equal the period lengths: $2, 8, 8, 18, 18, 32$.
background
The Periodic Table Engine implements the eight-tick octave of Recognition Science as chemical shell closures. Fixed block offsets (s, p, d, f) supply the valence contributions, and eight-window neutrality detects noble-gas closures in the cumulative ledger. The upstream Block inductive supplies the fixed φ-packing offsets for these blocks with no per-element tuning permitted.
proof idea
The proof is a one-line wrapper that applies native_decide to evaluate the arithmetic equality of the two explicit lists directly.
why it matters
This result verifies the Noble Gas Closure Theorem (P0-A0) stated in the module: noble gases occur exactly where the valence ledger returns to eight-window neutrality. It links the chemical eight-tick balance (T7) to the observed period lengths inside the zero-parameter scaffold. No downstream uses are recorded yet.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.