isHalogen
plain-language theorem explainer
The declaration defines the predicate isHalogen(Z) as membership of atomic number Z in the fixed list of halogen atomic numbers. Researchers deriving ionic bond formation from 8-tick shell closure in the Recognition Science framework cite this predicate to classify electron-accepting elements. The definition is a direct set-membership check against the list {9, 17, 35, 53, 85}.
Claim. The predicate isHalogen(Z) holds if and only if the atomic number Z belongs to the set {9, 17, 35, 53, 85}.
background
The IonicBond module derives ionic bonding from electron transfer between low-ionization-energy metals and high-electron-affinity non-metals, driven by 8-tick shell closure. Alkali metals donate electrons to reach noble-gas configuration while halogens accept one electron to complete their valence shell. The upstream definition halogenZ supplies the concrete list [9, 17, 35, 53, 85] of fluorine through astatine.
proof idea
One-line definition that expands directly to membership of Z in the halogenZ list.
why it matters
The predicate feeds the theorems fluorine_is_halogen, chlorine_is_halogen, bromine_is_halogen, iodine_is_halogen, astatine_is_halogen and halogen_ea_one. It supplies the classification step required by the RS ionic-bond mechanism (8-tick closure drive plus electron-affinity gain) and by the electronegativity-difference proxy used in lattice-energy estimates.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.