astatine_is_halogen
plain-language theorem explainer
Astatine with atomic number 85 satisfies the halogen predicate, defined as having distance to closure equal to one. Chemists applying Recognition Science to electron affinity ordering would cite this to fix astatine in the halogen group alongside fluorine through iodine. The proof is a one-line native decision that evaluates membership in the explicit halogen set derived from the closure condition.
Claim. The element with atomic number 85 satisfies the halogen predicate, i.e., its distance to noble-gas shell closure equals one.
background
The module derives electron affinity from φ-ladder scaling, where EA reflects the cost reduction when an atom approaches eight-tick neutrality. Halogens are defined as elements one electron short of closure, yielding the set {9, 17, 35, 53, 85}. The predicate isHalogen is introduced as distToClosure Z = 1 and equivalently as membership in that fixed set; upstream definitions in IonicBond and AnchorPolicyCertified supply the integer Z map and the decidable instance used for evaluation.
proof idea
The proof is a one-line wrapper that applies native_decide to the decidable predicate isHalogen at input 85, confirming membership in the halogen set without further reduction steps.
why it matters
This result anchors the halogen column in the Recognition Science periodic table, directly supporting the module's EA ordering (halogens > chalcogens > ... > noble gases) and the sign prediction for noble-gas EA. It instantiates the eight-tick octave closure mechanism from the forcing chain and supplies the concrete Z=85 case needed for downstream affinity calculations. No open scaffolding remains for this specific claim.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.