Chemistry Atomic Radii

Atomic radii

Atomic radius is the distance from an atom's nucleus to its outermost electron shell. In chemistry, this distance is not a fixed number; it changes with the element's position on the periodic table. Two trends dominate. Moving left to right across a period, radii shrink because the increasing positive charge of the nucleus pulls electrons closer. Moving down a group, radii grow because each new shell sits farther from the nucleus. A third trend, the lanthanide contraction, describes how filling the f-block orbitals causes a notable decrease in radius for the elements that follow.

The periodic table itself organizes elements into periods (rows) and groups (columns). Each period ends with a noble gas, an element with a full outer shell. For example, helium (Z=2), neon (Z=10), argon (Z=18), krypton (Z=36), xenon (Z=54), radon (Z=86), and oganesson (Z=118) all have valence electrons equal to their period length, a fact the framework's library verifies for each one. The elements just before a noble gas, the halogens, sit near a local minimum in radius, while the alkali metals that begin the next period show a sharp increase.

In Recognition Science, atomic radii are modeled through a ledger, a discrete record of recognition events, where the shell number n determines a base radius. The framework defines a shell radius proxy as phi^n, where phi is the golden ratio, approximately 1.618. This means each successive shell's base radius is larger by a factor of phi. A screening factor, which depends on the number of valence electrons relative to the period length, then adjusts this base value downward. The final radius proxy is the product of these two terms.

The framework's machine-checked library of formal theorems proves specific instances of these trends. It shows that lithium (Z=3) has a larger normalized radius than fluorine (Z=9), and sodium (Z=11) larger than chlorine (Z=17), confirming the period trend. It also proves that potassium (Z=19) has a higher shell number than lithium, confirming the group trend. For elements with a single valence electron, the library verifies that lithium, sodium, potassium, rubidium, cesium, and francium all have valenceElectrons equal to 1. The distance to the next noble gas closure is verified as 1 for fluorine, chlorine, bromine, iodine, and astatine, placing them one step before a full shell.

These results are formal theorems, not empirical measurements. The framework derives them from its definitions of shell number, screening factor, and normalized radius. The scaling law that shell radii follow powers of phi is a proved theorem, but the comparison of these proxies to actual measured atomic radii from experiment remains a separate empirical check. The framework's contribution is a consistent, formal model that reproduces the qualitative shape of the periodic table's radius trends.

/-- Noble gases have complete shells: valenceElectrons = periodLength. -/
theorem helium_full_shell : valenceElectrons 2 = periodLength 2 := by native_decide

theorem neon_full_shell : valenceElectrons 10 = periodLength 10 := by native_decide

theorem argon_full_shell : valenceElectrons 18 = periodLength 18 := by native_decide

theorem krypton_full_shell : valenceElectrons 36 = periodLength 36 := by native_decide

theorem xenon_full_shell : valenceElectrons 54 = periodLength 54 := by native_decide

theorem radon_full_shell : valenceElectrons 86 = periodLength 86 := by native_decide

theorem oganesson_full_shell : valenceElectrons 118 = periodLength 118 := by native_decide

/-- Li (Z=3) has larger radius than F (Z=9) in Period 2.
    Li: (1 - (3-2)/(10-2)) = 7/8
    F:  (1 - (9-2)/(10-2)) = 1/8 -/
theorem li_larger_than_f : normalizedRadius 3 > normalizedRadius 9 := by
  simp only [normalizedRadius, prevClosure, nextClosure]
  norm_num

/-- Na (Z=11) has larger radius than Cl (Z=17) in Period 3.
    Na: (1 - (11-10)/(18-10)) = 7/8
    Cl: (1 - (17-10)/(18-10)) = 1/8 -/
theorem na_larger_than_cl : normalizedRadius 11 > normalizedRadius 17 := by
  simp only [normalizedRadius, prevClosure, nextClosure]
  norm_num

/-- K (Z=19) has larger shell number than Li (Z=3) due to more shells. -/
theorem k_larger_shell_than_li : shellNumber 19 > shellNumber 3 := by
  native_decide

/-- Raw shell radius proxy: φ^(shell_number).
    Higher shell = larger base radius. -/
def shellRadiusProxy (Z : ℕ) : ℝ :=
  Constants.phi ^ (shellNumber Z : ℝ)

What this page does not claim

The framework does not measure atomic radii; its results are formal theorems about its own definitions. The framework does not derive the periodic table's structure from first principles; it assumes shell numbers and period lengths. The framework does not explain why screening follows the specific linear form it uses.

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