helium_full_shell
plain-language theorem explainer
Helium satisfies the closed-shell condition where valence electron count equals period length at atomic number 2. Modelers of atomic radii via phi-ladder scaling in Recognition Science cite this to anchor noble-gas maxima. The equality follows from direct evaluation of the two upstream definitions on the concrete input Z=2.
Claim. For atomic number 2, the valence electron count $Z - $prevClosure$(Z)$ equals the period length $ $nextClosure$(Z) - $prevClosure$(Z)$.
background
In the Chemistry.AtomicRadii module, atomic radii are derived from phi-ladder scaling with shell number. Period length for Z is defined as nextClosure(Z) minus prevClosure(Z). Valence electrons for Z is defined as Z minus prevClosure(Z), counting electrons past the prior noble-gas core. The module states that noble gases are exactly those elements where valence electrons equals period length, producing local radius maxima. This rests on the upstream PeriodicTable definitions of the closure functions that locate shell boundaries.
proof idea
One-line wrapper that applies native_decide to evaluate the concrete equality at Z=2 using the definitions of valenceElectrons and periodLength.
why it matters
The declaration confirms the Recognition Science insight that noble gases occur precisely when valence equals period length, here for the first case helium. It supports the atomic-radii model in which closed shells produce local maxima and alkali metals begin new shells. The result aligns with the phi-ladder mechanism for shell structure and the period/group trends stated in the module doc-comment.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.