module module high

`IndisputableMonolith.Chemistry.ElectronAffinity`

Defines electron-affinity proxies from distance to the next noble-gas shell closure on the eight-tick octave. RS chemistry modules and auditors cite the halogen EA=1 and noble-gas EA=0 lemmas as fit-free baselines. The file is mostly definitional scaffolding over the PeriodicTable engine, with short list-membership proofs for the halogen set.

claimElectron affinity is proxied by distance to the next noble-gas closure: $d(Z)$ equals the number of electrons needed to complete the shell. Normalized EA, an EA proxy, and halogen predicates are derived from $d(Z)$, with noble gases satisfying $\mathrm{EA}=0$ and halogens $\mathrm{EA}=1$.

background

Recognition Science chemistry sits on the eight-tick octave: shell closures (noble-gas "rests") are detected by an eight-window neutrality predicate on $\varphi$-tier rails with fixed s/p/d/f block offsets. No per-element tuning is allowed; the PeriodicTable engine supplies only that zero-parameter API.

This module takes distance-to-closure $d(Z)$ (electrons still needed to reach the next noble gas) as the fundamental proxy for electron affinity. From it one builds a raw EA proxy, a normalized version, and Boolean predicates identifying the halogen column. Constants supplies the RS tick $\tau_0=1$ used elsewhere in the chemistry stack, but EA itself is dimensionless here.

proof idea

Definition-heavy module. Core objects (distToClosure, eaProxy, normalizedEA, isHalogen, halogenZ) are pure defs over the PeriodicTable closure predicate. The short theorems noble_gas_ea_zero and halogen_ea_one discharge by unfolding those defs and using list-membership facts (fluorine_in_halogen_list, …, astatine_in_halogen_list). No deep algebraic argument; the content is the choice of proxy and the closed halogen enumeration.

why it matters in Recognition Science

Supplies the EA side of the classical Mulliken relation used downstream. Electronegativity (CH-008) sets $\mathrm{EN}\sim d(Z)^{-1}$ modulated by shell number, quoting distance-to-closure directly. IonicBond (CH-010) needs high-EA non-metals (halogens) opposite low-IE metals so that both ions reach 8-tick closure; the halogen EA=1 lemma anchors that drive. The module therefore sits between the fit-free PeriodicTable scaffold and the first quantitative bond-type predictions, keeping the eight-tick octave (T7) visible in chemistry.

scope and limits

Does not output absolute EA in eV or any dimensionful energy unit.
Does not fit or regress against experimental electron-affinity tables.
Does not treat anions beyond single-electron attachment to neutrals.
Does not derive EA from the J-cost functional; the proxy is combinatorial.
Halogen list is finite and explicit; no general proof for all Z in group 17.

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