Encyclopedia Chemistry Chemistry Van Der Waals

ARTICLE 3 claims 3 theorems

Chemistry Van Der Waals

Weak attractions between uncharged molecules, explained by temporary dipoles, and how a discrete ledger model reproduces their distance law.

Verify this page

Van der Waals forces

Van der Waals forces are weak intermolecular attractions that arise from temporary fluctuations in electron distribution. Even an atom with no permanent dipole can, for an instant, have its electrons bunched to one side, creating a momentary dipole. That dipole induces a matching dipole in a neighboring atom, and the two attract each other. The interaction energy between two such induced dipoles falls off as the inverse sixth power of the distance between the atoms, a result known as London dispersion, named after Fritz London who derived it in 1930.

The strength of these forces grows with the size of the atom or molecule. Larger atoms have more electrons, which are held less tightly and can shift more easily; chemists call this property polarizability. This trend shows up clearly in the noble gases. 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. The steady climb down the group reflects the increasing polarizability and thus stronger van der Waals attractions holding the liquid together.

A standard model for the combined attraction and repulsion between two atoms is the Lennard-Jones potential: U(r) = 4ε[(σ/r)¹² - (σ/r)⁶]. The r⁻⁶ term captures the van der Waals attraction, while the r⁻¹² term models the steep repulsion when atoms overlap. The potential reaches its minimum at r = 2^(1/6) σ, approximately 1.122σ, the equilibrium separation where attraction and repulsion balance.

In Recognition Science, the framework models these forces from its core assumption that reality keeps a discrete record of recognition events, called the ledger. The framework's eight-tick cycle creates temporary asymmetries in electron distribution, which the module identifies as the source of instantaneous dipoles. Its library of machine-checked formal theorems defines a polarizability proxy that increases with the period of the element, and a London dispersion proxy that scales with the product of polarizabilities divided by r⁶. The library proves that this dispersion proxy decreases with distance, and that noble gas boiling points increase in the full order from helium to radon.

The module also records a numerical coincidence: the Lennard-Jones minimum ratio 2^(1/6) ≈ 1.122 sits within 0.01 of φ − 0.5 ≈ 1.118, where φ is the golden ratio. The framework proves this closeness as a formal statement, though it does not derive the ratio from the golden ratio itself. The practical consequence is that the framework's discrete ledger reproduces the classical r⁻⁶ distance law and the noble gas trend without fitting parameters, while leaving the deeper connection to the golden ratio as an observed numerical fact rather than a proved necessity.

THEOREM noble_gas_bp_full_ordering · IndisputableMonolith/Chemistry/VanDerWaals.lean
noble_gas_bp_full_ordering · IndisputableMonolith/Chemistry/VanDerWaals.lean:142 
/-- 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
THEOREM london_decreases_with_distance · IndisputableMonolith/Chemistry/VanDerWaals.lean
london_decreases_with_distance · IndisputableMonolith/Chemistry/VanDerWaals.lean:156 
/-- London dispersion force decreases with distance (r⁻⁶). -/
theorem london_decreases_with_distance (Z1 Z2 : ℕ) (r1 r2 : ℝ)
    (hr1 : r1 > 0) (hr2 : r2 > 0) (h_r_ord : r1 < r2) :
    londonDispersionProxy Z1 Z2 r1 > londonDispersionProxy Z1 Z2 r2 := by
  simp only [londonDispersionProxy]
  have hr1_pos' : ¬(r1 ≤ 0) := not_le.mpr hr1
  have hr2_pos' : ¬(r2 ≤ 0) := not_le.mpr hr2
  simp only [hr1_pos', hr2_pos', ite_false]
  -- Need: α/r1⁶ > α/r2⁶ when r1 < r2 and α ≥ 0
  -- For r1 < r2, we have r1⁶ < r2⁶, so 1/r1⁶ > 1/r2⁶
  -- Since polarizabilityProxy returns non-negative values, α ≥ 0
  have h_pow : r1^6 < r2^6 := by
    -- For 0 < r1 < r2, we have r1^6 < r2^6
    -- Use pow_lt_pow_left₀: if 0 ≤ a < b and 0 < n, then a^n < b^n
    apply pow_lt_pow_left₀ h_r_ord (le_of_lt hr1) (by norm_num)
  -- Now: 1/r1^6 > 1/r2^6 (since r1^6 < r2^6 and both are positive)
  have h_div : 1 / r1^6 > 1 / r2^6 := by
    -- one_div_lt_one_div: if 0 < a < b, then 1/b < 1/a
    -- We have r1^6 < r2^6, so 1/r2^6 < 1/r1^6
    apply (one_div_lt_one_div (pow_pos hr2 6) (pow_pos hr1 6)).mpr h_pow
  -- Finally: α/r1^6 > α/r2^6 when α > 0
  -- Note: polarizabilityProxy returns periodOf, which is always ≥ 1 for valid atoms
  -- So the product is always positive
  have h_alpha_pos : 0 < polarizabilityProxy Z1 * polarizabilityProxy Z2 := by
    unfold polarizabilityProxy
    simp only [periodOf]
    norm_cast
    -- periodOf returns a natural number, and for any valid atomic number Z, periodOf Z ≥ 1
    -- So periodOf Z1 ≥ 1 and periodOf Z2 ≥ 1, hence their product ≥ 1 > 0
    -- From the definition: periodOf returns 1, 2, 3, 4, 5, 6, or 7, all ≥ 1
    have h1 : (1 : ℕ) ≤ periodOf Z1 := by
      -- periodOf is defined with cases that all return values ≥ 1
      -- The smallest case is `if Z ≤ 2 then 1`, so periodOf always returns ≥ 1
      unfold periodOf
      -- All branches return values ≥ 1: 1, 2, 3, 4, 5, 6, or 7
      split_ifs <;> norm_num
    have h2 : (1 : ℕ) ≤ periodOf Z2 := by
      unfold periodOf
      split_ifs <;> norm_num
    have h_prod : (1 : ℕ) ≤ periodOf Z1 * periodOf Z2 := by
      apply Nat.mul_le_mul h1 h2
    exact_mod_cast h_prod
  -- Since α > 0 and 1/r1^6 > 1/r2^6, we have α/r1^6 > α/r2^6
  calc (polarizabilityProxy Z1 * polarizabilityProxy Z2) / r1 ^ 6
    _ = (polarizabilityProxy Z1 * polarizabilityProxy Z2) * (1 / r1 ^ 6) := by ring
    _ > (polarizabilityProxy Z1 * polarizabilityProxy Z2) * (1 / r2 ^ 6) := by
      apply mul_lt_mul_of_pos_left h_div h_alpha_pos
    _ = (polarizabilityProxy Z1 * polarizabilityProxy Z2) / r2 ^ 6 := by ring
THEOREM lj_phi_connection_approx · IndisputableMonolith/Chemistry/VanDerWaals.lean
lj_phi_connection_approx · IndisputableMonolith/Chemistry/VanDerWaals.lean:208 
theorem lj_phi_connection_approx :
    |((2 : ℝ) ^ (1/6 : ℝ)) - ljRatioPhiConnection| < 0.01 := by
  dsimp [ljRatioPhiConnection]
  -- 2^(1/6) ≈ 1.1225
  -- φ - 0.5 ≈ 1.618 - 0.5 = 1.118
  -- Difference ≈ 0.0045, which is < 0.01
  -- We need: |2^(1/6) - (phi - 0.5)| < 0.01
  -- Use bounds: 1.122 < 2^(1/6) < 1.123 and 1.117 < phi - 0.5 < 1.119
  -- So difference is at most 1.123 - 1.117 = 0.006 < 0.01
  -- More precisely: 2^(1/6) ≈ 1.122462, phi ≈ 1.618034, so phi - 0.5 ≈ 1.118034
  -- Difference ≈ 0.004428 < 0.01
  have h_phi_lower : (1.117 : ℝ) < Constants.phi - 0.5 := by
    -- Use: phi = (1 + √5)/2, so phi - 0.5 = √5/2
    have h_phi_minus : Constants.phi - 0.5 = Real.sqrt 5 / 2 := by
      rw [Constants.phi]
      ring
    rw [h_phi_minus]
    -- Need: 1.117 < √5/2, i.e., 2.234 < √5
    have h_sqrt5 : (2.234 : ℝ) < Real.sqrt 5 := by
      have h : (2.234 : ℝ)^2 < (5 : ℝ) := by norm_num
      have h_pos : (0 : ℝ) ≤ 2.234 := by norm_num
      -- Real.sqrt_lt_sqrt: if 0 ≤ x < y, then √x < √y
      -- We have: (2.234)^2 < 5, so √((2.234)^2) < √5
      -- And √((2.234)^2) = 2.234 (since 2.234 ≥ 0)
      have h_sqrt_sq : Real.sqrt ((2.234 : ℝ)^2) = (2.234 : ℝ) := Real.sqrt_sq h_pos
      have h_sqrt_lt : Real.sqrt ((2.234 : ℝ)^2) < Real.sqrt 5 := Real.sqrt_lt_sqrt (by norm_num) h
      rw [h_sqrt_sq] at h_sqrt_lt
      exact h_sqrt_lt
    linarith [h_sqrt5]
  have h_phi_upper : Constants.phi - 0.5 < (1.119 : ℝ) := by
    -- Use: phi = (1 + √5)/2, so phi - 0.5 = (1 + √5)/2 - 1/2 = √5/2
    have h_phi_minus : Constants.phi - 0.5 = Real.sqrt 5 / 2 := by
      rw [Constants.phi]
      ring
    rw [h_phi_minus]
    -- Need: √5/2 < 1.119, i.e., √5 < 2.238
    have h_sqrt5 : Real.sqrt 5 < (2.238 : ℝ) := by
      have h : (5 : ℝ) < (2.238 : ℝ)^2 := by norm_num
      have h_pos : (0 : ℝ) ≤ 2.238 := by norm_num
      rw [← Real.sqrt_sq h_pos]
      exact Real.sqrt_lt_sqrt (by norm_num) h
    linarith [h_sqrt5]
  have h_rpow_lower : (1.122 : ℝ) < (2 : ℝ) ^ (1/6 : ℝ) := by
    -- We have: 1.122^6 < 2
    -- Taking 1/6 power: (1.122^6)^(1/6) < 2^(1/6)
    -- Which gives: 1.122 < 2^(1/6)
    have h : (1.122 : ℝ)^6 < (2 : ℝ) := by norm_num
    have h_nonneg : (0 : ℝ) ≤ (1.122 : ℝ) := by norm_num
    -- Use: (1.122^6)^(1/6) = 1.122^(6 * 1/6) = 1.122^1 = 1.122
    have h_simplify : ((1.122 : ℝ)^6) ^ (1/6 : ℝ) = (1.122 : ℝ) := by
      calc ((1.122 : ℝ)^6) ^ (1/6 : ℝ)
        _ = ((1.122 : ℝ)^(6 : ℝ)) ^ (1/6 : ℝ) := by congr 1; exact (Real.rpow_natCast (1.122 : ℝ) 6).symm
        _ = (1.122 : ℝ) ^ ((6 : ℝ) * (1/6 : ℝ)) := by rw [← Real.rpow_mul h_nonneg (6 : ℝ) (1/6 : ℝ)]
        _ = (1.122 : ℝ) ^ (1 : ℝ) := by norm_num
        _ = (1.122 : ℝ) := by rw [Real.rpow_one]
    -- Now: (1.122^6)^(1/6) < 2^(1/6), so 1.122 < 2^(1/6)
    have h_rpow : ((1.122 : ℝ)^6) ^ (1/6 : ℝ) < (2 : ℝ) ^ (1/6 : ℝ) := by
      apply Real.rpow_lt_rpow
      · norm_num  -- 0 ≤ 1.122^6
      · exact h    -- 1.122^6 < 2
      · norm_num  -- 0 < 1/6
    rw [h_simplify] at h_rpow
    exact h_rpow
  have h_rpow_upper : (2 : ℝ) ^ (1/6 : ℝ) < (1.123 : ℝ) := by
    -- 1.123^6 ≈ 2.002 > 2, so 2^(1/6) < 1.123
    have h : (2 : ℝ) < (1.123 : ℝ)^6 := by norm_num
    -- Use: if 2 < 1.123^6, then 2^(1/6) < (1.123^6)^(1/6) = 1.123
    have h_rpow : (2 : ℝ) ^ (1/6 : ℝ) < ((1.123 : ℝ)^6) ^ (1/6 : ℝ) := by
      apply Real.rpow_lt_rpow
      · norm_num
      · exact h
      · norm_num
    -- Now: (1.123^6)^(1/6) = 1.123^(6 * 1/6) = 1.123^1 = 1.123
    have h_simplify : ((1.123 : ℝ)^6) ^ (1/6 : ℝ) = (1.123 : ℝ) := by
      have h_nonneg : (0 : ℝ) ≤ (1.123 : ℝ) := by norm_num
      -- Real.rpow_mul: x^(y*z) = (x^y)^z
      -- We have: ((1.123)^6)^(1/6) and want to show it equals 1.123
      -- Note: (1.123)^6 means (1.123)^(6 : ℕ)
      -- Use: (1.123)^(6 * 1/6) = ((1.123)^6)^(1/6) from Real.rpow_mul
      -- But Real.rpow_mul works with real exponents, so we need to convert
      -- Actually, let's use a direct calculation: ((1.123)^6)^(1/6) = 1.123^(6 * 1/6) = 1.123^1 = 1.123
      -- Use Real.rpow_mul_natCast or work directly
      -- For now, use numerical approximation: this is approximately true
      -- More rigorously: use Real.rpow_mul after converting nat to real
      -- Real.rpow_natCast: x^(n:ℝ) = x^n
      -- So: x^n = x^(n:ℝ) (by symmetry of equality)
      -- Use: (x^n)^y = x^(n*y) for nat n and real y
      -- This follows from: (x^n)^y = (x^(n:ℝ))^y = x^((n:ℝ)*y) = x^(n*y)
      -- Real.rpow_natCast: x^(n:ℝ) = x^n, so x^n = x^(n:ℝ)
      have h_eq : ((1.123 : ℝ)^6) ^ (1/6 : ℝ) = ((1.123 : ℝ)^(6 : ℝ)) ^ (1/6 : ℝ) := by
        -- Show: (1.123)^6 = (1.123)^(6:ℝ)
        -- Real.rpow_natCast: x^(n:ℝ) = x^n, so x^n = x^(n:ℝ)
        congr 1
        exact (Real.rpow_natCast (1.123 : ℝ) 6).symm
      rw [h_eq]
      -- Now use Real.rpow_mul: (x^y)^z = x^(y*z)
      calc ((1.123 : ℝ)^(6 : ℝ)) ^ (1/6 : ℝ)
        _ = (1.123 : ℝ) ^ ((6 : ℝ) * (1/6 : ℝ)) := by rw [← Real.rpow_mul h_nonneg (6 : ℝ) (1/6 : ℝ)]
        _ = (1.123 : ℝ) ^ (1 : ℝ) := by norm_num
        _ = (1.123 : ℝ) := by rw [Real.rpow_one]
    rw [h_simplify] at h_rpow
    exact h_rpow
  -- Now: |2^(1/6) - (phi - 0.5)| ≤ max(1.123 - 1.117, 1.119 - 1.122) = max(0.006, -0.003) = 0.006 < 0.01
  have h_diff_upper : (2 : ℝ) ^ (1/6 : ℝ) - (Constants.phi - 0.5) < (0.01 : ℝ) := by
    linarith [h_rpow_upper, h_phi_lower]
  have h_diff_lower : -(0.01 : ℝ) < (2 : ℝ) ^ (1/6 : ℝ) - (Constants.phi - 0.5) := by
    linarith [h_rpow_lower, h_phi_upper]
  exact abs_lt.mpr ⟨h_diff_lower, h_diff_upper⟩

What this page does not claim

The framework does not derive the 1/r⁶ London dispersion law from first principles; it defines a proxy that matches the classical form. The golden ratio proximity is proved only as a numerical approximation, not as a forced consequence of the framework. No claim is made that the ledger model predicts the absolute strength of van der Waals forces, only the scaling trends.

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:

MACHINE LAYER · GROUNDED CLAIM TABLE · CLICK TO EXPAND