electronegativityDifference
The electronegativity difference proxy for atomic numbers Z1 and Z2 returns the absolute difference of their enProxy values unless either is zero. Chemists classifying bond ionicity in the Recognition Science setting cite this when checking alkali-halogen pairs against the ionic threshold. The definition is a direct case split that delegates to the upstream enProxy function.
claimLet $Z_1,Z_2$ be atomic numbers. Define the electronegativity difference proxy by $0$ if $Z_1=0$ or $Z_2=0$, otherwise by $|e(Z_1)-e(Z_2)|$ where $e(Z)$ is the electronegativity proxy $1/($distToNextClosure$(Z)+1)$ times $1/$shellNumber$(Z)$.
background
The IonicBond module derives ionic bonding from the 8-tick shell closure drive: alkali metals donate electrons to reach noble-gas configuration while halogens accept electrons to complete their valence shell. The upstream enProxy definition supplies the quantitative proxy: elements close to closure in small shells receive higher values, matching the qualitative ordering of real electronegativities. This difference therefore serves as the RS-native measure of electron-transfer tendency before lattice energy is considered.
proof idea
The definition performs an immediate case split on whether either argument is zero and returns zero in that branch; otherwise it evaluates the two calls to enProxy and takes the absolute value. No lemmas are invoked beyond the definition of enProxy itself.
why it matters in Recognition Science
This definition supplies the predicate body for isIonicBond and is invoked inside the proof of alkali_halogen_ionic, which asserts that all alkali-halogen pairs exceed the ionic threshold. It thereby operationalizes the 8-tick closure drive stated in the module doc and connects directly to T7 of the forcing chain. The construction closes the step from abstract RS mechanism to concrete chemical classification without new hypotheses.
scope and limits
- Does not incorporate measured ionization energies or electron affinities.
- Does not compute lattice energies or Madelung constants.
- Does not distinguish ionic geometries such as NaCl versus CsCl.
- Does not return absolute Pauling-scale electronegativities.
Lean usage
simp only [isIonicBond, electronegativityDifference, ionicThreshold]formal statement (Lean)
58def electronegativityDifference (Z1 Z2 : ℕ) : ℝ :=
proof body
Definition body.
59 if Z1 = 0 ∨ Z2 = 0 then 0
60 else
61 let en1 := enProxy Z1
62 let en2 := enProxy Z2
63 |en1 - en2|
64
65/-- Ionic character threshold (qualitative).
66 Bonds with EN difference > threshold are considered ionic.
67
68 Note: The enProxy function gives small fractional values (≈ 0.01-0.17),
69 so the threshold is correspondingly small. This captures the relative
70 difference between electronegativity proxy values, not absolute values.
71
72 **Numerical analysis** (computed externally):
73 - Alkali enProxy values: Li≈0.042, Na≈0.031, K≈0.011, Rb≈0.009, Cs≈0.004, Fr≈0.004
74 - Halogen enProxy values: F≈0.167, Cl≈0.125, Br≈0.100, I≈0.083, At≈0.071
75 - Minimum difference (Li-At): |0.042 - 0.071| ≈ 0.030 > 0.02 ✓
76 - Maximum difference (Fr-F): |0.004 - 0.167| ≈ 0.163 -/