Chemistry Ionization Energy Alkali Min Ionization

The alkali minimum

First ionization energy I₁(Z) is the energy needed to remove the outermost electron from a neutral atom of atomic number Z. In the periodic table, this energy rises across a period and then drops sharply at the start of the next. The lowest values in each period belong to the alkali metals: lithium, sodium, potassium, rubidium, cesium, and francium. Each has a single valence electron beyond a closed noble-gas core, and that electron is comparatively easy to remove. The highest values belong to the noble gases, whose outer shells are full.

This periodic structure is classical chemistry, taught in every introductory course. The Recognition Science framework, a machine-checked library of formal theorems, models the same pattern from a different starting point. It defines a dimensionless proxy for ionization energy: the number of valence electrons, with a value of 1 for an alkali metal and the period length for a noble gas. The framework then proves a small theorem, alkali_min_ionization, stating that any element with exactly one valence electron and atomic number greater than 2 has ionization proxy equal to 1. This is the formal statement that alkalis sit at the minimum of the sawtooth.

The theorem itself is a direct consequence of the definition: if the proxy is the valence count, then a valence count of 1 gives a proxy of 1. What matters is the surrounding structure. The framework also proves that the proxy increases monotonically within a period and that it resets at each period boundary, so the alkali after a noble gas always has a lower proxy than the noble gas before it. These ordering results are what the framework calls fit-free: they emerge from the definitions without tuning to measured data.

What the theorem does not claim is numerical accuracy. The proxy is a dimensionless ordering device, not a prediction of electron-volt values. The framework's own falsification criteria make this explicit: only the ordering of ionization energies is predicted, not their magnitudes. A measured violation of the ordering, say an alkali that does not have the minimum in its period, would falsify the model. The numerical values themselves require an external anchor and are not derived.

In plain terms, the declaration establishes a structural claim about the periodic table: within the framework's model, alkalis are provably the minimum-ionization elements of their periods. It does not establish that the framework's predicted ionization energies match measured values, nor does it derive the fine-structure constant or any other fundamental constant. The theorem is a formal statement about the model's internal consistency, not an empirical law.

/-- Within any period, alkali metals have minimum ionization proxy. -/
theorem alkali_min_ionization (Z : ℕ) (hZ : valenceElectrons Z = 1) (hZ2 : Z > 2) :
    ionizationProxy Z = 1 := by
  simp only [ionizationProxy]
  exact hZ

/-- Ionization proxy is monotone increasing within a period.
    If Z₁ < Z₂ are in the same period, then proxy(Z₁) < proxy(Z₂). -/
theorem ionization_monotone_within_period (Z1 Z2 : ℕ)
    (hZ1ge : Z1 ≥ prevClosure Z1)
    (hLt : Z1 < Z2) (hNotCross : prevClosure Z1 = prevClosure Z2) :
    ionizationProxy Z1 < ionizationProxy Z2 := by
  simp only [ionizationProxy, valenceElectrons]
  -- Z1 - prevClosure Z1 < Z2 - prevClosure Z2
  -- Since prevClosure Z1 = prevClosure Z2, this reduces to Z1 < Z2
  have hZ2ge : Z2 ≥ prevClosure Z2 := by omega
  omega

/-- 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

What this page does not claim

The theorem does not predict numerical ionization energies in electron volts. The theorem does not claim that the framework's ionization model matches measured data. The theorem does not derive the fine-structure constant or any other fundamental constant.

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: