window8Sum
plain-language theorem explainer
window8Sum defines the sliding sum of eight consecutive values of any function f starting at atomic number Z0. Modelers of chemical periodicity under Recognition Science cite it to implement the eight-window neutrality test that locates noble-gas closures. The definition is a direct one-line application of Finset.range sum over the interval from Z0 to Z0+7.
Claim. The sliding eight-window sum is given by $S(f,Z_0) = (Finset.range 8).sum (fun k => f(Z_0 + k))$ for a valence-cost proxy $f : ℕ → ℝ$.
background
The Periodic Table Engine in Chemistry.PeriodicTable supplies a zero-parameter scaffold that maps the eight-tick octave to chemical periods via phi-tier rails and fixed block offsets (s/p/d/f). window8Sum supplies the concrete sliding sum that feeds the neutrality predicate: noble gases are exactly the points where the running valence imbalance returns to zero inside an aligned 8-window. This construction is the chemical counterpart of the 8-tick ledger balance described in the module documentation as the deterministic closure condition under the RS scheduler.
proof idea
The declaration is a direct definition that expands to the Finset.sum of f(Z0 + k) for k ranging over 0 to 7. No lemmas are applied; the body is the canonical expression for a fixed-length window sum.
why it matters
window8Sum is the computational primitive that realizes the Noble Gas Closure Theorem (P0-A0) stated in the module documentation: the set {2,10,18,36,54,86} is forced by 8-window neutrality under a deterministic valence proxy. It directly supports the downstream definitions neutralAt and neutralAt_const_zero and thereby connects to the eight-tick octave (T7) in the forcing chain. The definition closes the interface between the abstract 8-tick ledger and concrete atomic-number arithmetic without introducing free parameters.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.