xenon_full_shell
plain-language theorem explainer
Xenon at atomic number 54 satisfies the closed-shell condition where its valence electron count equals the length of its period. Chemists modeling atomic radii under Recognition Science would cite this to verify the noble-gas closure rule. The proof reduces the equality to ground arithmetic via native_decide on the definitions of prevClosure and nextClosure.
Claim. For atomic number 54, the valence electron count equals the period length: valence electrons of 54 equals period length for 54.
background
Recognition Science constructs the periodic table via closure points that mark the ends of periods. Period length for Z is defined as nextClosure(Z) minus prevClosure(Z). Valence electrons for Z are Z minus prevClosure(Z), counting electrons beyond the prior noble-gas core. The module documentation states that noble gases occur exactly where these quantities coincide, producing complete shells and local radius maxima. The upstream definitions in PeriodicTable supply the arithmetic for both functions.
proof idea
The proof is a one-line wrapper that invokes the native_decide tactic to evaluate the equality directly on natural-number arithmetic.
why it matters
This equality confirms the RS insight, quoted in the valenceElectrons doc-comment, that noble gases are those elements where valence count matches period length. It anchors the predicted local maxima for noble gases in the atomic-radii trends derived from φ-ladder scaling. No downstream theorems depend on it, indicating it functions as a verification checkpoint rather than an active lemma. It aligns with the period-decrease and group-increase trends stated in the module documentation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.