 262  { rail := (period : ℤ), block := b }
 263
 264/- Dimensionless predicted band multiplier for atomic number `Z`. -/
 265def bandMultiplier (Z : ℕ) [BlockOffsets] : ℝ :=
 266  let idx := indexOf Z
 267  blockFactor idx.rail idx.block
 268
 269/-- Predicted (dimensionful) band energy for atomic number `Z`.
 270    This is a fit‑free display using the universal coherence tick. -/
 271def bandEnergy (Z : ℕ) [BlockOffsets] : ℝ :=
 272  IndisputableMonolith.Constants.E_coh * bandMultiplier Z
 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

papers checked against this theorem

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