halogenZ
plain-language theorem explainer
halogenZ enumerates the atomic numbers of the five halogens for electron-affinity calculations in the Recognition Science framework. Researchers modeling shell-closure effects on the phi-ladder cite this list to identify elements one electron short of noble-gas neutrality. The entry is a direct list definition with no lemmas or reductions applied.
Claim. The atomic numbers of the halogens are $9, 17, 35, 53, 85$.
background
Electron affinity is modeled in this module as the energy gain from approaching eight-tick shell closure on the phi-ladder. The upstream definition distToClosure(Z) returns the number of electrons needed to reach the next noble-gas configuration and serves as the direct proxy for affinity strength. The predicate isHalogen holds precisely when this distance equals one, matching the physical pattern that halogens release the most energy upon electron addition while noble gases sit at zero distance.
proof idea
The declaration is a direct definition that returns the constant list [9, 17, 35, 53, 85]. No lemmas are invoked and no tactics are executed; the body simply supplies the enumeration of fluorine through astatine.
why it matters
The list supplies the concrete set required by the downstream membership theorems for each halogen and by the alkali-halogen ionic-bond theorem that compares electronegativity proxies. It implements the module's sign-prediction rule that halogens lie one step from closure and therefore exhibit high affinity, consistent with the eight-tick octave in the unified forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.