 273
 274/- Eight‑window neutrality predicate (rest if the sum is zero in aligned windows).
 275     In practice, the neutrality test is applied to a fit‑free valence‑cost proxy. -/
 276def neutralAt (f : ℕ → ℝ) (Z0 : ℕ) : Prop :=
 277  window8Sum f Z0 = 0
 278
 279/-- Trivial sanity: a constant‑zero proxy is neutral on any aligned 8‑window. -/
 280theorem neutralAt_const_zero (Z0 : ℕ) :
 281  neutralAt (fun _ => (0 : ℝ)) Z0 := by
 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

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.