krypton_full_shell
plain-language theorem explainer
Krypton at atomic number 36 satisfies the closed-shell condition in which valence electron count equals period length under Recognition Science shell definitions. Chemists modeling atomic radii via phi-ladder scaling cite this to confirm noble-gas closure points. The verification reduces to native computation of the closure functions at Z=36.
Claim. For atomic number 36, the valence electron count equals the period length: $36 - p(36) = n(36) - p(36)$, where $p$ denotes the previous closure and $n$ the next closure.
background
The module derives atomic radii from phi-ladder scaling, with radii decreasing across periods due to increasing nuclear charge and increasing down groups as new shells open. Period length for element Z is defined as nextClosure(Z) minus prevClosure(Z). Valence electrons for Z is Z minus prevClosure(Z), so that noble gases occur exactly where these two quantities coincide, marking complete shells.
proof idea
The proof is a one-line wrapper that invokes the native_decide tactic on the concrete natural-number expressions obtained by unfolding valenceElectrons and periodLength at Z=36.
why it matters
This result instantiates the Recognition Science claim that noble gases are those elements where valence electrons equal period length, anchoring the local maxima in atomic radii predicted by the module. It supports the phi-ladder mechanism for shell structure without invoking external constants. No downstream theorems depend on it in the current graph.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.