neutralAt
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.
claimLet $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 in Recognition Science
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.
scope and limits
- Does not prescribe any concrete form for the valence proxy function f.
- Does not prove that the observed noble-gas sequence {2,10,18,36,54,86} arises for any particular f.
- Does not incorporate empirical mass or energy data.
- Does not extend beyond the eight-window sliding sum.
formal statement (Lean)
276def neutralAt (f : ℕ → ℝ) (Z0 : ℕ) : Prop :=
proof body
Definition body.
277 window8Sum f Z0 = 0
278
279/-- Trivial sanity: a constant‑zero proxy is neutral on any aligned 8‑window. -/