fluorine_is_halogen
plain-language theorem explainer
Fluorine with atomic number 9 satisfies the halogen predicate, defined via distance to closure equaling one on the phi-ladder. Chemists using Recognition Science electron-affinity predictions would cite this to place fluorine at the high-affinity end of each period. The verification reduces to a single native decision step on the finite halogen list.
Claim. The atomic number 9 satisfies the halogen predicate, i.e., the distance from 9 to the nearest noble-gas closure equals 1.
background
The module derives electron affinity from phi-ladder scaling toward eight-tick neutrality. Halogens are those elements one electron short of closure, so they exhibit high affinity by completing the shell at low cost. The predicate isHalogen is defined as distToClosure Z = 1, with the explicit set {9, 17, 35, 53, 85}. Upstream results supply the closure-distance function and the anchor map Z from the Masses module.
proof idea
One-line wrapper that applies native_decide to the finite membership test for the halogen set.
why it matters
The result anchors the halogen classification required for the module's EA ordering (halogens > chalcogens > ... > noble gases) and the sign prediction for noble-gas affinities. It directly supports the T7 eight-tick octave and the approach-to-closure mechanism stated in the module doc. No downstream uses are recorded yet.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.