`neutralAt_const_zero`

proved

show as: view math explainer →

module: IndisputableMonolith.Chemistry.PeriodicTable
domain: Chemistry
line: 280 · github
papers citing: none yet

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.Chemistry.PeriodicTable on GitHub at line 280.

browse module

All declarations in this module, on Recognition.

explainer page

A cached Ask Recognition explainer exists for this declaration.

open explainer

depends on

formal source

 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
 307end IndisputableMonolith

papers checked against this theorem

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