theorem
proved
tactic proof
neutralAt_const_zero
show as:
view Lean formalization →
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