chlorine_is_halogen
plain-language theorem explainer
Chlorine with atomic number 17 satisfies the halogen predicate, defined via distance to closure equaling one. Modelers of electron affinity under Recognition Science φ-ladder scaling cite this to fix the third-period halogen assignment. The proof is a one-line native decision that evaluates the decidable membership predicate directly.
Claim. The predicate isHalogen(17) holds, where isHalogen(Z) means distToClosure(Z) = 1 (equivalently, Z belongs to the set {9, 17, 35, 53, 85}).
background
The Electron Affinity module models EA as the cost reduction when an atom approaches 8-tick neutrality on the φ-ladder. Halogens are defined as elements one electron short of closure, so they exhibit high EA; noble gases sit at closure and show near-zero or negative EA. The predicate isHalogen(Z) is introduced as distToClosure(Z) = 1 and is also realized by explicit membership in the halogen list {9, 17, 35, 53, 85}.
proof idea
The proof is a one-line term proof that invokes native_decide on the decidable predicate isHalogen 17, which reduces to list membership or distance computation.
why it matters
This instance anchors the halogen classification for Z = 17 inside the Recognition Science chemistry layer, directly supporting the module's EA ordering (halogens highest within each period) and the 8-tick neutrality mechanism. It supplies a concrete data point for normalizedEA and related scaling formulas without adding hypotheses. The result closes one leaf of the halogen list while leaving the general φ-ladder derivation open.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.