f_dist_one
plain-language theorem explainer
The declaration shows that the distance to the next noble gas closure for atomic number 9 equals 1. Chemists applying Recognition Science to atomic radii would cite this fact to locate halogens immediately before period closure in the phi-ladder model. The proof is a one-line wrapper that invokes native_decide on the definition of distance to next closure.
Claim. Let $d(Z)$ denote the distance in atomic number to the next noble gas closure. Then $d(9) = 1$.
background
The module derives atomic radii from phi-ladder scaling. Radii decrease across a period as Z rises and increase down a group with new shells. Halogens sit near the minimum radius for their period because they lie one step before shell closure. The upstream definition states: distance to next noble gas closure equals nextClosure Z minus Z, and equals zero precisely at noble gases where the shell is complete.
proof idea
The proof is a one-line wrapper that applies native_decide to evaluate distToNextClosure 9 directly from its definition as nextClosure 9 minus 9.
why it matters
This instance anchors the halogen placement predicted by the phi-ladder scaling of atomic radii. It supplies a concrete check for the period trend in which radii reach a local minimum just before noble-gas closure. The result sits inside the Chemistry.AtomicRadii module and supports downstream radius proxies that combine shell number with screening.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.