neutralAt_const_zero
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.
claimLet $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 in Recognition Science
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.
scope and limits
- Does not establish neutrality for any non-constant valence proxy.
- Does not link the zero function to measured atomic properties or element data.
- Does not constrain predicted period lengths or shell capacities.
- Does not address the falsification criteria listed in the module for non-trivial proxies.
formal statement (Lean)
280theorem neutralAt_const_zero (Z0 : ℕ) :
281 neutralAt (fun _ => (0 : ℝ)) Z0 := by
proof body
Tactic-mode proof.
282 unfold neutralAt window8Sum
283 simpa using (by
284 have : (Finset.range 8).sum (fun _ => (0 : ℝ)) = 0 := by
285 simpa using (Finset.sum_const_zero (Finset.range 8))
286 exact this)
287
288/-! ## Falsification Criteria
289
290The noble gas closure theorem is falsifiable:
291
2921. **Wrong closures**: If the valence proxy predicts closures (neutralAt = true)
293 at non-noble-gas Z values within the first 118 elements.
294
2952. **Missed closures**: If the valence proxy fails to achieve neutrality at
296 known noble gas positions.
297
2983. **Period length mismatch**: If predicted period lengths diverge from
299 observed {2, 8, 8, 18, 18, 32, 32}.
300
301These are testable by the validation script `scripts/analysis/chem_noble_gas_closure.py`.
302-/
303
304end
305end PeriodicTable
306end Chemistry
307end IndisputableMonolith