neutralAt
plain-language theorem explainer
neutralAt defines the eight-window neutrality predicate on a valence-cost proxy f at atomic number Z0. Periodic-table modelers in the Recognition Science scaffold cite it to locate noble-gas closures via ledger balance. The definition is a direct one-line abbreviation equating the predicate to the window sum equaling zero.
Claim. Let $f : ℕ → ℝ$ be a valence proxy and $Z_0 ∈ ℕ$. Then neutralAt($f$, $Z_0$) holds precisely when $∑_{k=0}^7 f(Z_0 + k) = 0$.
background
The Periodic Table module supplies a fit-free scaffold that maps the eight-tick octave onto chemistry via φ-tier rails and fixed block offsets (s=0, p=1, d=2, f=3). window8Sum computes the sliding sum of any proxy function over eight consecutive atomic numbers. The module documentation states that noble gases are exactly the elements where cumulative valence cost achieves 8-window neutrality, realizing the 8-tick ledger balance in the chemical domain.
proof idea
The definition is a direct abbreviation that unfolds neutralAt to the equality window8Sum f Z0 = 0. No tactics or lemmas are applied beyond the window sum definition itself.
why it matters
neutralAt supplies the neutrality test required by the Noble Gas Closure Theorem (P0-A0) described in the module documentation. It is used by the downstream theorem neutralAt_const_zero, which verifies that the constant-zero proxy satisfies the condition on any aligned window. The predicate thereby embeds the eight-tick neutrality condition (T7) into the chemistry engine without introducing parameters.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.