cl_dist_one
plain-language theorem explainer
The declaration records that chlorine (Z=17) sits one position before the argon closed shell. Atomic-radius modelers working with phi-ladder shell scaling cite this fact when tabulating valence distances for halogens. The proof is a one-line wrapper that evaluates the distance function by native computation.
Claim. Let $d(Z)$ be the number of steps from atomic number $Z$ to the next noble-gas closure. Then $d(17)=1$.
background
The AtomicRadii module derives radii from phi-ladder scaling: base radius grows with shell number while effective radius shrinks with added valence electrons. The upstream definition states that distToNextClosure(Z) equals nextClosure(Z) minus Z and equals zero precisely when Z is a noble gas. The module therefore treats this distance as the remaining valence count that controls screening and radius contraction across each period.
proof idea
The proof is a one-line wrapper that applies native_decide to the arithmetic definition of distToNextClosure at input 17.
why it matters
The result supplies the concrete valence distance for chlorine inside the Chemistry.AtomicRadii development, supporting the predicted minimum radius just before shell closure. It instantiates the PeriodicTable distance function for a specific halogen but has no recorded downstream uses, so its integration into radiusProxy or normalizedRadius remains open.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.