halogenZ
plain-language theorem explainer
The atomic numbers of the halogens are enumerated as nine, seventeen, thirty-five, fifty-three and eighty-five. Ionic bond derivations in Recognition Science cite this list to identify electron acceptors that complete an eight-tick shell. The declaration is a direct list literal with no computation or lemmas applied.
Claim. The halogens correspond to the atomic numbers $9$, $17$, $35$, $53$, $85$.
background
The Ionic Bond module derives bonding from electron transfer between alkali metals and halogens, driven by eight-tick shell closure. Alkali metals donate to reach noble-gas configuration while halogens accept one electron to finish their valence shell. The list supplies the acceptor atomic numbers. The identical enumeration appears upstream in the Electron Affinity module to support membership predicates.
proof idea
Direct definition via list literal.
why it matters
This definition supports the alkali-halogen ionic predicate and the individual membership theorems for fluorine through astatine. It encodes the high-affinity elements that reach eight-tick closure by electron gain, consistent with the Recognition Science forcing chain and the module's RS mechanism for lattice energy.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.