def
definition
def or abbrev
electronegativityDifference
show as:
view Lean formalization →
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 -/