module module high

`IndisputableMonolith.Chemistry.Electronegativity`

Electronegativity module supplies a Recognition Science proxy for EN derived from distance to the next 8-tick shell closure on the phi-ladder. Periodic trend models and ionic bonding derivations cite these definitions to rank elements by electron attraction strength. The module assembles proxy functions and ranking lemmas from upstream atomic radii and electron affinity results using the formula EN ~ 1/(distToNextClosure + 1) scaled by inverse shell number.

claimElectronegativity proxy: $EN(Z) = [1/ (d_{next}(Z) + 1)] / n_{shell}$, where $d_{next}(Z)$ is the distance in phi-ladder steps to the next noble-gas closure and $n_{shell}$ is the principal shell index. Elements near closure in low shells receive the highest values.

background

The module operates inside the Chemistry domain of Recognition Science, which maps the eight-tick octave (T7) onto periodic blocks via the PeriodicTable engine. That upstream module supplies an eight-window neutrality predicate to detect noble-gas closures and a fixed set of s/p/d/f block offsets with no per-element tuning. AtomicRadii and ElectronAffinity supply the period-decrease and closure-approach patterns that feed the proxy. Constants fixes the base time quantum as tau_0 = 1 tick.

proof idea

this is a definition module, no proofs

why it matters in Recognition Science

The module supplies the electronegativity component required by the IonicBond derivation (CH-010), which models electron transfer as driven by mutual 8-tick closure seeking between cation and anion. It completes the CH-009 slot in the chemistry chain by providing a zero-parameter EN ranking that downstream bonding and reactivity lemmas can invoke directly.

scope and limits

Does not compute experimental Pauling or Mulliken electronegativity numbers.
Does not incorporate relativistic or spin-orbit effects for heavy atoms.
Does not model solvent or molecular-environment shifts to EN.
Does not predict bond energies or reaction rates.

used by (1)

From the project-wide theorem graph. These declarations reference this one in their body.

IndisputableMonolith.Chemistry.IonicBond module_import

depends on (4)

Lean names referenced from this declaration's body.

IndisputableMonolith.Chemistry.AtomicRadii module_import
IndisputableMonolith.Chemistry.ElectronAffinity module_import
IndisputableMonolith.Chemistry.PeriodicTable module_import
IndisputableMonolith.Constants module_import

declarations in this module (18)

def enProxy L36
def enRanking L43
theorem fluorine_gt_li L50
theorem fluorine_gt_be L54
theorem fluorine_gt_b L58
theorem fluorine_gt_c L62
theorem fluorine_gt_n L66
theorem fluorine_gt_o L70
theorem chlorine_gt_sodium L74
theorem en_increases_across_period L79
theorem group_17_en_order L92
theorem alkali_min_valence L97
theorem cesium_low_en L104
theorem carbon_intermediate L109
theorem nitrogen_ranking L114
theorem oxygen_ranking L119
theorem fluorine_ranking L124
theorem noble_gas_zero_en L131