Encyclopedia Chemistry Chemistry Electron Affinity
ARTICLE 4 claims 3 theorems 1 model
Chemistry Electron Affinity
Electron affinity measures the energy released when an atom gains an electron; in Recognition Science it is modeled as the distance to the next noble gas closure.
Electron affinity as a distance
Electron affinity is the energy released when a neutral atom gains an electron to become a negative ion. It is a central quantity in chemistry because it ranks how strongly atoms attract additional electrons. The halogens, which sit one electron short of a filled shell, release the most energy; noble gases, already at a filled shell, release almost none or even absorb energy. This ordering is a textbook fact, and it is the pattern the Recognition Science framework starts from.
The framework models electron affinity as a simple distance: the number of electrons an atom needs to reach the next noble gas configuration. An atom with atomic number Z has a proxy value equal to that distance, called eaProxy. For a halogen the distance is exactly 1, for a noble gas it is exactly 0. The framework proves these two endpoint facts in its machine-checked library: halogen_ea_one and noble_gas_ea_zero. It also proves that within a single period, as Z increases toward the closure, the proxy value strictly decreases, and that the halogen at the end of a period has the maximum affinity in that period.
In Recognition Science, this distance is not a free parameter. It follows from the framework's central result that any cost function satisfying five plain conditions must equal J(x) = (x + 1/x)/2 - 1. From that cost function the framework derives an eight-tick recognition cycle, which it identifies with the period length of the periodic table, and the distance to closure is the natural measure of how far an atom is from completing a cycle. The framework's claim is that electron affinity is the cost reduction from approaching that eight-tick neutrality: adding an electron to a halogen completes a shell and releases energy, while adding one to a noble gas starts a new shell and costs energy.
The module also defines a normalized electron affinity, dividing the distance by the period length, so that values are comparable across periods. The results in the module are checked by the framework's library; they establish the ordering predictions: halogens have the highest affinity within a period, noble gases have zero or negative affinity, and affinity decreases as an atom moves toward closure. The comparison against measured electron affinities is an empirical check, not a formal result.
THEOREM halogen_ea_one · noble_gas_ea_zero · IndisputableMonolith/Chemistry/ElectronAffinity.lean
/-- Halogens have EA proxy = 1 (one electron completes shell). -/
theorem halogen_ea_one (Z : ℕ) (h : isHalogen Z) : eaProxy Z = 1 := by
simp only [eaProxy, distToClosure]
exact h
/-- Noble gases have EA proxy = 0 (at closure, no benefit from adding electron). -/
theorem noble_gas_ea_zero (Z : ℕ) (h : isNobleGas Z) : eaProxy Z = 0 := by
simp only [eaProxy, distToClosure]
exact noble_gas_at_closure Z h
THEOREM ea_decreases_within_period · IndisputableMonolith/Chemistry/ElectronAffinity.lean
/-- Within a period, EA proxy decreases as Z increases (filling the shell).
Elements closer to closure have higher EA potential. -/
theorem ea_decreases_within_period (Z1 Z2 : ℕ)
(hZ1le : Z1 ≤ nextClosure Z1)
(hZ2le : Z2 ≤ nextClosure Z2)
(hLt : Z1 < Z2)
(hSame : nextClosure Z1 = nextClosure Z2) :
eaProxy Z1 > eaProxy Z2 := by
simp only [eaProxy, distToClosure, distToNextClosure]
omega
THEOREM halogen_max_ea · IndisputableMonolith/Chemistry/ElectronAffinity.lean
/-- Halogens have higher EA proxy than any other non-noble element in their period. -/
theorem halogen_max_ea (Z : ℕ) (Z' : ℕ)
(hZle : Z ≤ nextClosure Z)
(_ : Z' ≤ nextClosure Z')
(hSamePeriod : nextClosure Z = nextClosure Z')
(hZ'lt : Z' < nextClosure Z') :
distToNextClosure Z' ≤ distToNextClosure Z ↔ Z ≤ Z' := by
simp only [distToNextClosure]
omega
MODEL eaProxy · IndisputableMonolith/Chemistry/ElectronAffinity.lean
/-- Electron affinity proxy: higher when closer to closure.
EA_proxy = periodLength - valenceElectrons = distToClosure
Halogens (dist=1) have highest proxy, noble gases (dist=0) have lowest. -/
def eaProxy (Z : ℕ) : ℕ := distToClosure Z
What this page does not claim
This answer does not claim that the framework derives the measured numerical values of electron affinities in electron volts. This answer does not claim that the distance proxy is the same as the quantum-mechanical electron affinity. This answer does not claim that the framework explains exceptions such as the higher affinity of chlorine over fluorine.
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/ElectronAffinity.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:
- How does the eight-tick cycle map onto the actual period lengths of the periodic table?
- What physical mechanism connects the cost function J to the energy released in electron attachment?
- Can the framework derive the sign of electron affinity for elements beyond the noble gases?
MACHINE LAYER · GROUNDED CLAIM TABLE · CLICK TO EXPAND
THEOREM halogen_ea_one · noble_gas_ea_zero · IndisputableMonolith/Chemistry/ElectronAffinity.lean
/-- Halogens have EA proxy = 1 (one electron completes shell). -/ theorem halogen_ea_one (Z : ℕ) (h : isHalogen Z) : eaProxy Z = 1 := by simp only [eaProxy, distToClosure] exact h/-- Noble gases have EA proxy = 0 (at closure, no benefit from adding electron). -/ theorem noble_gas_ea_zero (Z : ℕ) (h : isNobleGas Z) : eaProxy Z = 0 := by simp only [eaProxy, distToClosure] exact noble_gas_at_closure Z hFor a halogen the distance is exactly 1, for a noble gas it is exactly 0. halogen_ea_one · noble_gas_ea_zero · IndisputableMonolith/Chemistry/ElectronAffinity.leanTHEOREM ea_decreases_within_period · IndisputableMonolith/Chemistry/ElectronAffinity.lean
/-- Within a period, EA proxy decreases as Z increases (filling the shell). Elements closer to closure have higher EA potential. -/ theorem ea_decreases_within_period (Z1 Z2 : ℕ) (hZ1le : Z1 ≤ nextClosure Z1) (hZ2le : Z2 ≤ nextClosure Z2) (hLt : Z1 < Z2) (hSame : nextClosure Z1 = nextClosure Z2) : eaProxy Z1 > eaProxy Z2 := by simp only [eaProxy, distToClosure, distToNextClosure] omegaWithin a single period, as Z increases toward the closure, the proxy value strictly decreases. ea_decreases_within_period · IndisputableMonolith/Chemistry/ElectronAffinity.leanTHEOREM halogen_max_ea · IndisputableMonolith/Chemistry/ElectronAffinity.lean
/-- Halogens have higher EA proxy than any other non-noble element in their period. -/ theorem halogen_max_ea (Z : ℕ) (Z' : ℕ) (hZle : Z ≤ nextClosure Z) (_ : Z' ≤ nextClosure Z') (hSamePeriod : nextClosure Z = nextClosure Z') (hZ'lt : Z' < nextClosure Z') : distToNextClosure Z' ≤ distToNextClosure Z ↔ Z ≤ Z' := by simp only [distToNextClosure] omegaThe halogen at the end of a period has the maximum affinity in that period. halogen_max_ea · IndisputableMonolith/Chemistry/ElectronAffinity.leanMODEL eaProxy · IndisputableMonolith/Chemistry/ElectronAffinity.lean
/-- Electron affinity proxy: higher when closer to closure. EA_proxy = periodLength - valenceElectrons = distToClosure Halogens (dist=1) have highest proxy, noble gases (dist=0) have lowest. -/ def eaProxy (Z : ℕ) : ℕ := distToClosure ZThe comparison against measured electron affinities is an empirical check, not a formal result. eaProxy · IndisputableMonolith/Chemistry/ElectronAffinity.lean