isHalogen
plain-language theorem explainer
An atomic number Z qualifies as a halogen exactly when the distance to the next noble gas shell closure equals one. Researchers predicting electron affinities from the phi-ladder scaling would invoke this predicate to flag species with maximal EA proxy. The declaration is a direct one-line definition that reuses the upstream distance function without further reduction or computation.
Claim. An atomic number $Z$ is a halogen if and only if the distance to the next noble gas closure satisfies $distToClosure(Z)=1$.
background
The module sets electron affinity as the energy released on shell completion, with RS predicting high EA for halogens (one electron short of closure), near-zero EA for noble gases (at closure), and low EA for alkali metals (one past closure). The mechanism ties EA to cost reduction when approaching eight-tick neutrality. distToClosure is defined as the number of electrons needed to reach the next noble gas shell and serves as the direct proxy: EA_proxy equals period length minus valence electrons, so halogens receive the highest proxy value while noble gases receive the lowest.
proof idea
The declaration is a direct definition that sets the predicate isHalogen Z to the equality distToClosure Z = 1. It performs no reduction and simply re-exports the upstream distance function.
why it matters
This predicate supplies the classification used by halogen_ea_one (which proves eaProxy Z = 1 under the hypothesis) and by the concrete theorems fluorine_is_halogen, chlorine_is_halogen, bromine_is_halogen, iodine_is_halogen, and astatine_is_halogen. It implements the RS claim that halogens approach eight-tick neutrality at minimal cost, consistent with the T7 eight-tick octave and the EA ordering Halogens > Chalcogens > ... > Noble gases. The definition closes the interface needed for the sign prediction that noble gases have EA ≤ 0.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.