Chemistry Van Der Waals Noble Gas Bp Full Ordering

The noble gas boiling point ladder

The noble gases are the six elements in the far right column of the periodic table: helium, neon, argon, krypton, xenon, and radon. Their boiling points, the temperatures at which they turn from liquid to gas, rise steadily down the group. Helium boils at 4.22 kelvin, neon at 27.07, argon at 87.30, krypton at 119.93, xenon at 165.05, and radon at 211.4 kelvin. The pattern is a standard fact of chemistry, taught in introductory courses because it illustrates how intermolecular forces grow with atomic size.

The physical reason is van der Waals forces, weak attractions between uncharged atoms that arise from temporary fluctuations in their electron clouds. A larger atom has more electrons spread over a bigger volume, so its cloud distorts more easily. That higher polarizability, the ease with which an electron cloud deforms, produces stronger attractions between neighboring atoms. Stronger attractions mean more energy is needed to separate the atoms, so the boiling point rises. The same logic explains why the interaction energy falls off as the sixth power of distance, a relation known as London dispersion.

In Recognition Science, the framework's machine-checked library of formal theorems encodes this trend as a proof. The declaration noble_gas_bp_full_ordering states, as a single theorem, that the boiling point of each noble gas is less than the boiling point of the next one down the group: helium below neon, neon below argon, argon below krypton, krypton below xenon, and xenon below radon. The proof chains together five smaller theorems, one for each adjacent pair, and each of those reduces to arithmetic on the defined boiling point values. The result is a formal certificate that the ordering holds for the six elements as listed.

The theorem certifies the ordering of these six specific numbers. It does not derive the boiling point values themselves from first principles, and it does not explain why polarizability increases with atomic size. Those are inputs to the framework, chosen as definitions rather than proved. The connection between the golden ratio and the Lennard-Jones minimum distance, a separate observation in the same file, is a numerical proximity, not a proved equality. The ordering proof stands on its own as a checkable statement about the listed temperatures, and it matches the measured trend that chemists have known for over a century.

/-- Complete ordering of noble gas boiling points. -/
theorem noble_gas_bp_full_ordering :
    nobleGasBoilingPoint 2 < nobleGasBoilingPoint 10 ∧
    nobleGasBoilingPoint 10 < nobleGasBoilingPoint 18 ∧
    nobleGasBoilingPoint 18 < nobleGasBoilingPoint 36 ∧
    nobleGasBoilingPoint 36 < nobleGasBoilingPoint 54 ∧
    nobleGasBoilingPoint 54 < nobleGasBoilingPoint 86 := by
  refine ⟨?_, ?_, ?_, ?_, ?_⟩
  · exact noble_gas_bp_increases_he_ne
  · exact noble_gas_bp_increases_ne_ar
  · exact noble_gas_bp_increases_ar_kr
  · exact noble_gas_bp_increases_kr_xe
  · exact noble_gas_bp_increases_xe_rn

/-- Noble gas boiling points increase down the group (vdW strength increases). -/
theorem noble_gas_bp_increases_he_ne : nobleGasBoilingPoint 2 < nobleGasBoilingPoint 10 := by
  simp only [nobleGasBoilingPoint]
  norm_num

theorem noble_gas_bp_increases_ne_ar : nobleGasBoilingPoint 10 < nobleGasBoilingPoint 18 := by
  simp only [nobleGasBoilingPoint]
  norm_num

theorem noble_gas_bp_increases_ar_kr : nobleGasBoilingPoint 18 < nobleGasBoilingPoint 36 := by
  simp only [nobleGasBoilingPoint]
  norm_num

theorem noble_gas_bp_increases_kr_xe : nobleGasBoilingPoint 36 < nobleGasBoilingPoint 54 := by
  simp only [nobleGasBoilingPoint]
  norm_num

theorem noble_gas_bp_increases_xe_rn : nobleGasBoilingPoint 54 < nobleGasBoilingPoint 86 := by
  simp only [nobleGasBoilingPoint]
  norm_num

/-- Complete ordering of noble gas boiling points. -/
theorem noble_gas_bp_full_ordering :
    nobleGasBoilingPoint 2 < nobleGasBoilingPoint 10 ∧
    nobleGasBoilingPoint 10 < nobleGasBoilingPoint 18 ∧
    nobleGasBoilingPoint 18 < nobleGasBoilingPoint 36 ∧
    nobleGasBoilingPoint 36 < nobleGasBoilingPoint 54 ∧
    nobleGasBoilingPoint 54 < nobleGasBoilingPoint 86 := by
  refine ⟨?_, ?_, ?_, ?_, ?_⟩
  · exact noble_gas_bp_increases_he_ne
  · exact noble_gas_bp_increases_ne_ar
  · exact noble_gas_bp_increases_ar_kr
  · exact noble_gas_bp_increases_kr_xe
  · exact noble_gas_bp_increases_xe_rn

What this page does not claim

The theorem does not derive the boiling point values from first principles; they are defined inputs. The theorem does not prove that polarizability increases with atomic size. The phi connection to the Lennard-Jones minimum is a numerical proximity within 0.01, not a proved equality.

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