halogen_ea_one
plain-language theorem explainer
Halogens are defined to lie exactly one electron short of noble-gas shell closure, forcing their electron affinity proxy to equal one by substitution. Recognition Science modelers of periodic trends would cite this when ranking EA values across periods or deriving shell-closure costs. The proof is a one-line term that rewrites eaProxy to distToClosure and discharges the hypothesis directly.
Claim. For any natural number $Z$ such that $Z$ is a halogen, the electron affinity proxy of $Z$ equals 1.
background
Electron affinity in this module is modeled as the cost reduction when an atom approaches eight-tick shell closure on the phi-ladder. The definition distToClosure(Z) returns the number of electrons needed to reach the next noble gas; eaProxy(Z) is set identically to that distance. The predicate isHalogen(Z) holds precisely when this distance equals one, identifying the set {9, 17, 35, 53, 85}.
proof idea
The term proof applies simp to unfold eaProxy and distToClosure, then uses exact to match the supplied hypothesis that distToClosure Z equals one.
why it matters
This pins the maximum EA proxy value for halogens, supporting the module's predicted ordering Halogens > Chalcogens > Pnictogens > Noble gases. It closes the halogen case in the phi-ladder approach to shell closure and aligns with the eight-tick neutrality from the forcing chain T7. No downstream theorems depend on it yet.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.