electronegativityDifference
plain-language theorem explainer
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.
Claim. Let $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
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.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.