radon_full_shell
plain-language theorem explainer
Radon (Z=86) meets the closed-shell condition where valence electron count equals period length. Chemists modeling RS-based atomic radii or periodic trends would cite this as a concrete check on noble-gas closure. The verification is a direct computational decision on the unfolded closure definitions.
Claim. For atomic number 86, the valence electron count beyond the prior noble-gas core equals the period length: $v(86)=p(86)$, where $v(Z)=Z-c_0$ and $p(Z)=c_1-c_0$ with $c_0$, $c_1$ the nearest closure points.
background
The module AtomicRadii derives radii from φ-ladder scaling under Recognition Science. Radii decrease across a period from rising nuclear charge and increase down a group from new shells; noble gases show local maxima from closed shells. The upstream definitions are periodLength(Z) := nextClosure Z - prevClosure Z and valenceElectrons(Z) := Z - prevClosure Z. The supplied insight states that noble gases are exactly those elements where valence count equals period length.
proof idea
One-line wrapper that applies native_decide to the equality after the closure functions are unfolded for Z=86.
why it matters
The declaration supplies a concrete instance of closed-shell verification inside the chemistry module, supporting the RS claim that noble gases produce radius maxima via complete shells (CH-007). It sits downstream of the PeriodicTable closure functions and aligns with the framework's shell-structure mechanism for radii. No downstream uses are recorded, so its role in full radius formulas remains an open extension.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.