module module high

`IndisputableMonolith.Chemistry.ElectronAffinity`

This module supplies the distance to the next noble-gas closure as the zero-parameter proxy for electron affinity inside the Recognition Science chemistry scaffold. It builds directly on the eight-tick periodic-table engine and the RS time quantum. Researchers deriving electronegativity or ionic-bond strengths from shell structure cite these definitions. The module contains only definitions and simple lemmas with no non-trivial proofs.

claimThe closure distance $d(Z)$ for atomic number $Z$ equals the number of electrons required to reach the next noble-gas configuration under the eight-tick octave rule; electron-affinity proxies are then formed as $eaProxy(Z) = f(d(Z))$ for suitable scaling functions $f$.

background

The module sits inside the Recognition Science chemistry framework that maps the periodic table to an eight-tick octave via φ-tier rails and fixed block offsets (s/p/d/f). Noble-gas closures are identified by an eight-window neutrality predicate with no per-element tuning. The sole imported constant is the RS time quantum τ₀ = 1 tick.

proof idea

this is a definition module, no proofs

why it matters in Recognition Science

The definitions feed the electronegativity derivation (CH-008), where EN scales as the inverse closure distance modulated by shell number, and the ionic-bond construction (CH-010), which uses the 8-tick closure drive for both cation and anion formation.

scope and limits

Does not incorporate measured electron-affinity data.
Does not extend the model beyond eight-tick shell closures.
Does not produce numerical EA values without additional scaling factors.
Does not address relativistic or multi-electron correlation effects.

used by (2)

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

IndisputableMonolith.Chemistry.Electronegativity module_import
IndisputableMonolith.Chemistry.IonicBond module_import

depends on (2)

Lean names referenced from this declaration's body.

IndisputableMonolith.Chemistry.PeriodicTable module_import
IndisputableMonolith.Constants module_import

declarations in this module (21)

def distToClosure L35
def eaProxy L40
def normalizedEA L45
def isHalogen L50
def halogenZ L53
theorem noble_gas_ea_zero L62
theorem halogen_ea_one L67
theorem fluorine_in_halogen_list L72
theorem chlorine_in_halogen_list L75
theorem bromine_in_halogen_list L78
theorem iodine_in_halogen_list L81
theorem astatine_in_halogen_list L84
theorem ea_decreases_within_period L90
theorem halogen_max_ea L100
theorem fluorine_is_halogen L112
theorem chlorine_is_halogen L115
theorem bromine_is_halogen L118
theorem iodine_is_halogen L121
theorem astatine_is_halogen L124
theorem neon_ea_zero L127
theorem argon_ea_zero L130