bromine_is_halogen
plain-language theorem explainer
Bromine with atomic number 35 satisfies the halogen predicate, defined via distance to closure equaling one. Chemists using Recognition Science electron affinity models would cite this to place bromine in the group with high predicted EA. The proof is a one-line native decision procedure that evaluates the predicate by direct computation on the fixed halogen set.
Claim. $35$ satisfies the halogen predicate, i.e., $distToClosure(35)=1$.
background
The Electron Affinity module derives EA from phi-ladder scaling toward 8-tick neutrality. Halogens are defined by the predicate $isHalogen(Z) := distToClosure(Z)=1$, with the explicit set {9, 17, 35, 53, 85}. This encodes elements one electron short of noble-gas closure, yielding low cost for shell completion and thus high EA. The module states EA ordering as halogens greater than chalcogens greater than pnictogens, with noble gases at or below zero. Upstream, the IonicBond sibling defines the same predicate via membership in halogenZ, confirming consistency with the distToClosure formulation.
proof idea
The proof is a one-line wrapper that applies the native_decide tactic to the decidable proposition isHalogen 35, which reduces to membership check against the halogen set and returns true.
why it matters
This result verifies bromine's position in the halogen group, directly supporting the CH-006 claim that halogens exhibit high electron affinity from approach to 8-tick closure on the phi-ladder. It supplies a concrete instance for the periodic table predictions in the module, where EA follows cost reduction to neutrality. No downstream theorems depend on it yet, and it touches no open scaffolding.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.