neutralAt_const_zero
plain-language theorem explainer
The theorem shows that the constant-zero function satisfies the eight-window neutrality predicate at every starting atomic number. Researchers modeling noble-gas closures under the Recognition Science valence ledger would cite it as the baseline case confirming that a null proxy produces exact rest points. The proof is a direct unfolding of the window sum followed by the standard finite-sum fact that eight zero terms add to zero.
Claim. Let $f : ℕ → ℝ$ be the constant function $f(n) = 0$. For every natural number $Z_0$, the eight-window sum satisfies $∑_{k=0}^{7} f(Z_0 + k) = 0$.
background
The PeriodicTable module implements an octave-to-eight-tick mapping for chemistry via φ-tier rails and a fixed set of block offsets. The central predicate is the eight-window neutrality test: window8Sum f Z0 equals the sum of f over the eight consecutive integers starting at Z0, and neutralAt f Z0 holds precisely when that sum is zero. This construction detects noble-gas closures as ledger balance points under the deterministic valence proxy, without per-element fitting. The module doc states that noble gases are exactly the elements where cumulative valence cost achieves 8-window neutrality, the chemical counterpart of the 8-tick ledger balance.
proof idea
The tactic proof first unfolds neutralAt and window8Sum to expose the Finset sum. It then introduces the auxiliary fact that the sum of the constant-zero function over Finset.range 8 is zero, which follows immediately from the library lemma Finset.sum_const_zero. The final simpa step discharges the goal with this identity.
why it matters
The result supplies the trivial base case for the Noble Gas Closure Theorem (P0-A0) described in the module documentation. It verifies that the neutrality predicate behaves correctly on the zero proxy, consistent with the eight-tick octave (T7) in the UnifiedForcingChain. No downstream theorems are recorded, so the declaration functions strictly as an internal sanity check rather than a load-bearing lemma.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.