enProxy
plain-language theorem explainer
enProxy defines a real-valued electronegativity proxy for atomic number Z as zero when Z equals zero or at noble gas closure, otherwise one over (distToNextClosure Z plus one) times one over shellNumber Z. Chemists applying Recognition Science to bonding criteria cite it for element rankings and ionic thresholds. The definition is a direct conditional expression that composes the upstream distance and shell functions without additional lemmas.
Claim. For atomic number $Z$, the electronegativity proxy equals $0$ if $Z=0$ or if the distance to the next noble gas closure is zero; otherwise it equals $1/(d_Z+1)cdot 1/n_Z$, where $d_Z$ is the distance to next closure and $n_Z$ is the shell number.
background
The module develops electronegativity from φ-ladder scaling (CH-008). Electronegativity measures an atom's tendency to attract electrons, with the RS mechanism EN ~ distToNextClosure^{-1} modulated by shell number. Classical relation is EN ~ sqrt(IE × EA) on the Mulliken scale. Upstream, shellNumber Z is defined as periodOf Z + 1, the 1-indexed shell for radii scaling. distToNextClosure Z equals nextClosure Z minus Z and is zero precisely at noble gases. periodLength and valenceElectrons supply related period structure.
proof idea
The definition is a direct piecewise expression: it returns zero for Z=0 or when distToNextClosure Z =0, otherwise scales the reciprocal of (distToNextClosure Z +1) by the reciprocal of shellNumber Z. It applies the upstream definitions of distToNextClosure and shellNumber with no further lemmas or tactics.
why it matters
This definition supplies the core proxy used by noble_gas_zero_en to prove noble gases have zero EN proxy and by electronegativityDifference together with isIonicBond to quantify ionic character in alkali-halogen pairs. It realizes the module predictions that fluorine has highest EN, EN increases across periods, and noble gases are undefined. It connects to phi-ladder scaling for chemical properties and the eight-tick octave structure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.