Chemistry Periodic Table Neutral At Const Zero

The trivial neutrality case

The periodic table organizes elements by atomic number, with rows called periods and columns called groups. A noble gas, such as helium (2) or neon (10), sits at the end of a period, and chemists say its outer electron shell is full. In the Recognition Science framework, a ledger, a discrete record of events, tracks a running balance. For chemistry, the framework defines a neutrality condition: a function is neutral at a position if the sum of its values over the next eight positions equals zero. This eight-window neutrality is meant to detect shell closures, the points where a noble gas appears.

The declaration neutralAt_const_zero proves a simple fact: the constant function that returns zero at every atomic number is neutral at every position. The proof is immediate from the definition, because the sum of eight zeros is zero. This is a sanity check on the framework's own definitions, not a discovery about real elements. It confirms that the neutrality predicate is not vacuously false and that the basic arithmetic of the eight-window sum behaves as expected.

In Recognition Science, the framework models noble gases as exactly those elements where the cumulative valence cost achieves eight-window neutrality. The set {2, 10, 18, 36, 54, 86} is forced by the requirement that shell closures occur at neutrality points under a deterministic valence proxy, with no per-element tuning. The framework's machine-checked library of formal theorems also proves that each of these six elements is noble, that the period lengths are the gaps between them, and that a noble gas has zero distance to the next closure. These are the substantive claims.

The neutrality result for the zero function does not say anything about actual elements. It does not predict a noble gas, does not assign a valence cost, and does not establish that any real element is neutral. It is a trivial theorem about a degenerate function, useful only to verify that the neutrality predicate is consistent. The chemical content of the framework lies elsewhere, in the theorems that connect the noble gas list to shell closures and period lengths.

/-- Trivial sanity: a constant‑zero proxy is neutral on any aligned 8‑window. -/
theorem neutralAt_const_zero (Z0 : ℕ) :
  neutralAt (fun _ => (0 : ℝ)) Z0 := by
  unfold neutralAt window8Sum
  simpa using (by
    have : (Finset.range 8).sum (fun _ => (0 : ℝ)) = 0 := by
      simpa using (Finset.sum_const_zero (Finset.range 8))
    exact this)

/-- Predicted (dimensionful) band energy for atomic number `Z`.
    This is a fit‑free display using the universal coherence tick. -/
def bandEnergy (Z : ℕ) [BlockOffsets] : ℝ :=
  IndisputableMonolith.Constants.E_coh * bandMultiplier Z

/- Eight‑window neutrality predicate (rest if the sum is zero in aligned windows).
     In practice, the neutrality test is applied to a fit‑free valence‑cost proxy. -/
def neutralAt (f : ℕ → ℝ) (Z0 : ℕ) : Prop :=
  window8Sum f Z0 = 0

/-- The canonical noble gas atomic numbers (first 6 periods + Oganesson). -/
def nobleGasZ : List ℕ := [2, 10, 18, 36, 54, 86]

What this page does not claim

The zero function is not a model of any real element's valence cost. The neutrality theorem does not predict the existence of any noble gas. The framework does not derive the periodic table from first principles without the valence proxy.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/Chemistry/PeriodicTable.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red: