eaProxy
plain-language theorem explainer
eaProxy(Z) returns the integer distance in electrons from atomic number Z to the next noble gas shell closure. Chemists working with Recognition Science periodic trends cite it to derive that halogens maximize electron affinity within each period while noble gases minimize it. The definition is a direct one-line alias to distToClosure, inheriting its value from the upstream closure arithmetic.
Claim. For atomic number $Z$, the electron affinity proxy is defined by $eaProxy(Z) := d(Z)$, where $d(Z)$ equals the number of electrons needed to reach the next shell closure.
background
Recognition Science models electron affinity as the energy gain from approaching shell closure on the φ-ladder. distToClosure(Z) computes exactly that deficit, serving as the fundamental proxy: halogens sit at distance 1 and noble gases at distance 0. The module CH-006 states that EA equals the cost reduction from approaching 8-tick neutrality, with the ordering halogens > chalcogens > ... > noble gases following directly from this distance.
proof idea
One-line wrapper that applies distToClosure: eaProxy Z := distToClosure Z. All subsequent properties (zero for noble gases, one for halogens) are inherited without additional reduction.
why it matters
The proxy supplies the concrete input for the downstream theorems noble_gas_ea_zero, halogen_ea_one, and ea_decreases_within_period. It operationalizes the CH-006 claim that EA tracks approach to closure, linking the PeriodicTable closure functions to the eight-tick octave (T7) and the J-cost ledger from PhiForcingDerived.of. It closes the interface between abstract periodicity and the falsifiable EA sign predictions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.