Chemistry Ionization Energy Sawtooth Reset

The sawtooth reset

First ionization energy is the energy needed to remove one electron from a neutral atom. In the periodic table, this energy rises as you move left to right across a row, then falls abruptly when you start the next row. The drop happens because a new electron shell begins: the first element of a new row, an alkali metal, holds its outer electron loosely, while the previous element, a noble gas, has a filled shell that is hard to break. This rise-and-drop pattern is the sawtooth.

The ionization energy sawtooth is a standard fact of chemistry, visible in any plot of measured values. The Recognition Science framework, a system that derives physical structure from a forced cost function, models this pattern with a simple proxy: it counts the number of valence electrons as a stand-in for ionization difficulty. Within a row, the proxy runs from 1 for an alkali metal up to the row length for a noble gas. The framework's machine-checked library of formal theorems contains a statement, sawtooth_reset, that captures the reset: for any noble gas and the alkali metal that follows it in the periodic table, the proxy for the alkali is strictly less than the proxy for the noble gas.

The theorem itself is narrow. It does not compute actual ionization energies in electronvolts. It does not assert that the framework's predicted numerical values match measured data. It states only an ordering fact: the proxy value drops when crossing a period boundary. The framework's own documentation is explicit that the numerical values are not predicted without an anchor; only the ordering is claimed to be fit-free. The theorem is proved by checking each of the six noble gas cases directly, from helium to oganesson, using the definition of noble gas and the successor relationship between the two elements.

What the theorem does not claim is as important as what it proves. It does not claim that the proxy equals the real ionization energy. It does not claim that the ordering holds for every pair of elements, only for the specific pair of a noble gas and its immediate successor. It does not claim that the framework's model is physically true; the model is a definitional choice, and the theorem is a consequence of that choice. The framework's own falsification criteria are stated separately: if measured data ever showed an alkali metal with higher ionization energy than the preceding noble gas, the model would be falsified.

In plain terms, the declaration establishes a formal guarantee about a model's internal consistency: within the framework's simplified picture, the sawtooth reset is not an assumption but a derived consequence. The reader can see that the framework is not merely asserting the pattern; it is proving that its own definitions force the pattern. Whether that pattern matches the real world is a separate question, one the framework leaves open for empirical testing.

/-- The sawtooth pattern: ionization resets at each period boundary.
    After a noble gas, the next element (alkali) has minimal ionization. -/
theorem sawtooth_reset (Znoble Zalkali : ℕ)
    (hNoble : isNobleGas Znoble)
    (hNext : Zalkali = Znoble + 1)
    (hValid : Zalkali ≤ 118) :
    ionizationProxy Zalkali < ionizationProxy Znoble := by
  -- Noble gas has maximum (= period length), alkali has 1
  -- Case by case on which noble gas
  unfold isNobleGas nobleGasZ at hNoble
  simp only [List.mem_cons, List.mem_nil_iff, or_false] at hNoble
  obtain rfl | rfl | rfl | rfl | rfl | rfl := hNoble <;>
    subst hNext <;>
    native_decide

/-- Predicted ionization energy in eV (display seam).
    Uses E_coh as the universal energy anchor. -/
def predictedI1_eV (Z : ℕ) : ℝ :=
  Constants.E_coh * scaledIonization Z * 1000  -- Scale factor for eV range

What this page does not claim

The theorem does not assert that the proxy equals the actual measured ionization energy. The theorem does not claim the ordering holds for any pair of elements within a period, only for a noble gas and its immediate successor. The framework does not claim the model is physically true; it is a definitional choice.

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/IonizationEnergy.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: