Chemistry Ionization Energy Scaled Ionization

The scaled ionization formula

First ionization energy is the energy needed to remove one electron from a neutral atom. It rises across a row of the periodic table, then drops sharply at the start of the next row, producing a sawtooth pattern. The Recognition Science framework models this pattern with a dimensionless quantity called scaled ionization, a number computed from an element's position in its period and the framework's fundamental scaling constant φ (the golden ratio, about 1.618).

The formula has two parts. The position factor is simply the element's number of valence electrons divided by its period length, so it runs from 1/n for an alkali metal to 1.0 for a noble gas. The rail factor multiplies this by φ raised to twice the period number, which the framework derives from its φ-ladder scaling law. The declaration scaledIonization in the framework's machine-checked library of formal theorems defines this product as a real number for any atomic number Z.

What the framework proves is an ordering, not numerical values. Its library contains formal theorems that within any period the ionization proxy increases monotonically with atomic number, that alkali metals have the minimum proxy value of 1, and that noble gases have the maximum equal to the period length. A separate theorem shows the sawtooth reset: the element immediately after a noble gas has a strictly smaller proxy than the noble gas itself. These ordering results are machine-checked, meaning the library's kernel verified the proofs.

The framework is explicit about what it does not claim. The numerical values of ionization energies in electron volts are not predicted without an anchor: the display formula multiplies by a cohesion energy constant and a scale factor, but the framework states plainly that only the ordering is fit-free. The model would be falsified if measured data showed an alkali metal that is not the minimum in its period, a noble gas that is not the maximum, or any within-period ordering violation beyond experimental error.

In Recognition Science, this scaled ionization is a display seam rather than a derived physical law. It packages the framework's structural predictions about periodicity into a single dimensionless number. What a reader can take away is a clear, testable claim: the periodic table's ionization sawtooth should follow the φ-rail ordering, and that claim stands or falls on measured data, not on the framework's internal consistency.

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

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

/-- Noble gases have maximum ionization proxy (equal to period length). -/
theorem noble_max_ionization (Z : ℕ) (h : isNobleGas Z) :
    ionizationProxy Z = periodLength Z := by
  simp only [ionizationProxy]
  exact noble_gas_complete_shell Z h

/-- 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 framework does not predict absolute ionization energies in electron volts without an external anchor. The framework does not claim that its φ-scaling law is a conventional physics derivation. The framework does not claim that its ordering theorems have been empirically verified against all measured data.

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: