Encyclopedia Chemistry Chemistry Ionic Bond Electronegativity Difference

ARTICLE 4 claims 2 theorems 2 models

Chemistry Ionic Bond Electronegativity Difference

Ionic bonds form when the electronegativity gap between two atoms passes a threshold; here is what that threshold is and what it leaves open.

Verify this page

The electronegativity difference

Electronegativity difference is the classic chemistry yardstick for predicting whether two atoms will form an ionic bond, where electrons transfer from one atom to the other. The usual rule, taught in every introductory course, is that a large difference, generally above 1.7 on the Pauling scale, favors ionic bonding, while a small difference favors covalent sharing. The Recognition Science framework encodes this same idea in a machine-checked library of formal theorems, but with a deliberately simpler threshold and a precise definition of what counts as a difference.

The declaration electronegativityDifference, a definition in the framework's chemistry module, takes two atomic numbers and returns the absolute value of the difference between their proxy electronegativity values. If either atomic number is zero, the difference is defined to be zero. The framework then calls a bond ionic when this difference exceeds a fixed threshold of 0.02, a value chosen for the formal model rather than derived from measurement. This is a definitional choice, not a theorem about the physical world.

What the framework does prove, as a theorem, is that any alkali metal paired with any halogen always clears this threshold. The proof relies on two smaller facts: alkali metals have exactly one valence electron, and halogens are one electron short of shell closure. The theorem alkali_halogen_ionic states that for any alkali metal Z_alkali and any halogen Z_halogen, the bond is ionic by the framework's definition. This matches the textbook expectation that sodium and chlorine, for instance, form an ionic compound.

The framework also defines a proxy for lattice energy, the electrostatic attraction that holds the ions together, and proves that this energy increases with ion charge. The Madelung constants for common crystal structures, such as sodium chloride at 1.748 and cesium chloride at 1.763, appear as fixed numbers in the library. These are inputs to the model, not results derived from it.

In Recognition Science, the framework models the electron transfer as driven by an eight-tick shell closure drive, where atoms seek a complete valence shell. The net energy change is ionization energy minus electron affinity, modulated by lattice energy. This is the framework's way of restating the standard Born-Haber cycle, not a new physical law. The framework's contribution is to make the textbook rule precise and machine-checkable, not to discover a new chemistry.

MODEL electronegativityDifference · IndisputableMonolith/Chemistry/IonicBond.lean
electronegativityDifference · IndisputableMonolith/Chemistry/IonicBond.lean:56 
/-- Electronegativity difference proxy.
    Higher values indicate more ionic character. -/
def electronegativityDifference (Z1 Z2 : ℕ) : ℝ :=
  if Z1 = 0 ∨ Z2 = 0 then 0
  else
    let en1 := enProxy Z1
    let en2 := enProxy Z2
    |en1 - en2|
MODEL isIonicBond · ionicThreshold · IndisputableMonolith/Chemistry/IonicBond.lean
isIonicBond · IndisputableMonolith/Chemistry/IonicBond.lean:79 
/-- Predicate: A bond between Z1 and Z2 is predominantly ionic. -/
def isIonicBond (Z1 Z2 : ℕ) : Prop :=
  electronegativityDifference Z1 Z2 > ionicThreshold
ionicThreshold · IndisputableMonolith/Chemistry/IonicBond.lean:65 
/-- Ionic character threshold (qualitative).
    Bonds with EN difference > threshold are considered ionic.

    Note: The enProxy function gives small fractional values (≈ 0.01-0.17),
    so the threshold is correspondingly small. This captures the relative
    difference between electronegativity proxy values, not absolute values.

    **Numerical analysis** (computed externally):
    - Alkali enProxy values: Li≈0.042, Na≈0.031, K≈0.011, Rb≈0.009, Cs≈0.004, Fr≈0.004
    - Halogen enProxy values: F≈0.167, Cl≈0.125, Br≈0.100, I≈0.083, At≈0.071
    - Minimum difference (Li-At): |0.042 - 0.071| ≈ 0.030 > 0.02 ✓
    - Maximum difference (Fr-F): |0.004 - 0.167| ≈ 0.163 -/
def ionicThreshold : ℝ := 0.02
THEOREM alkali_halogen_ionic · IndisputableMonolith/Chemistry/IonicBond.lean
alkali_halogen_ionic · IndisputableMonolith/Chemistry/IonicBond.lean:83 
/-- Alkali-halogen pairs form ionic bonds.
    This is a physical fact: alkali metals have low EN, halogens have high EN,
    and their electronegativity difference exceeds the ionic threshold.

    **Numerical verification** (30 cases):
    - All alkali enProxy values are ≤ 0.042 (Li has highest)
    - All halogen enProxy values are ≥ 0.071 (At has lowest)
    - Minimum |difference| = |0.042 - 0.071| ≈ 0.030 > 0.02 ✓

    **Proof status**: Requires Real arithmetic case analysis.
    The 30 cases involve noncomputable division, so native_decide fails.
    norm_num with simp can handle the expanded forms. -/
theorem alkali_halogen_ionic (Z_alkali Z_halogen : ℕ)
    (h_alkali : isAlkaliMetal Z_alkali) (h_halogen : isHalogen Z_halogen) :
    isIonicBond Z_alkali Z_halogen := by
  simp only [isIonicBond, electronegativityDifference, ionicThreshold]
  simp only [isAlkaliMetal, alkaliMetalZ, isHalogen, halogenZ] at h_alkali h_halogen
  have haz : Z_alkali ≠ 0 := by
    simp only [List.mem_cons, List.mem_nil_iff, or_false] at h_alkali
    rcases h_alkali with rfl | rfl | rfl | rfl | rfl | rfl <;> norm_num
  have hhz : Z_halogen ≠ 0 := by
    simp only [List.mem_cons, List.mem_nil_iff, or_false] at h_halogen
    rcases h_halogen with rfl | rfl | rfl | rfl | rfl <;> norm_num
  simp only [haz, hhz, false_or, ↓reduceIte]
  -- The proof requires numerical case analysis on 30 alkali-halogen pairs
  -- Each case reduces to showing |1/(d₁+1)/s₁ - 1/(d₂+1)/s₂| > 0.02
  -- where d = distToNextClosure and s = shellNumber
  --
  -- Key insight: All halogen enProxy ≥ 1/14 (At), all alkali enProxy ≤ 1/24 (Li)
  -- Minimum difference: 1/14 - 1/24 = 5/168 > 1/50 = 0.02
  simp only [List.mem_cons, List.mem_nil_iff, or_false] at h_alkali h_halogen
  -- Expand enProxy for each specific case
  rcases h_alkali with rfl | rfl | rfl | rfl | rfl | rfl <;>
  rcases h_halogen with rfl | rfl | rfl | rfl | rfl <;>
  simp only [enProxy, distToNextClosure, nextClosure, AtomicRadii.shellNumber, periodOf,
             ↓reduceIte, OfNat.ofNat_ne_zero] <;>
  norm_num
THEOREM lattice_energy_increases_with_charge · IndisputableMonolith/Chemistry/IonicBond.lean
lattice_energy_increases_with_charge · IndisputableMonolith/Chemistry/IonicBond.lean:146 
/-- Lattice energy proxy increases with ionic charge product.
    U(1,1) < U(2,1) since 1/d < 2/d for d > 0. -/
theorem lattice_energy_increases_with_charge (d : ℝ) (hd : d > 0) :
    latticeEnergyProxy 1 1 d < latticeEnergyProxy 2 1 d := by
  simp only [latticeEnergyProxy]
  have hd_pos : ¬(d ≤ 0) := not_le.mpr hd
  simp only [hd_pos, ite_false]
  -- 1/d < 2/d when d > 0
  have h1 : (1 : ℤ).toNat = 1 := rfl
  have h2 : (2 : ℤ).toNat = 2 := rfl
  simp only [h1, h2]
  -- 1 * 1 / d < 2 * 1 / d when d > 0
  have : (1 : ℝ) * 1 / d < 2 * 1 / d := by
    apply div_lt_div_of_pos_right _ hd
    norm_num
  simpa using this

What this page does not claim

The framework does not derive the numerical value of the electronegativity threshold from any deeper principle. The framework does not claim that its electronegativity proxy reproduces measured Pauling electronegativities. The framework does not prove that any specific real-world compound, such as sodium chloride, forms an ionic bond; it only proves a statement about its own formal definitions.

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