oganesson_full_shell
plain-language theorem explainer
Oganesson (Z=118) satisfies the noble-gas closure condition: its valence electron count equals the length of its period. Modelers of Recognition Science shell structure cite this as the terminal case confirming that valence equals period length at full shells. The proof is a direct native_decide evaluation of the two period-table functions.
Claim. For atomic number 118, the valence electron count $Z - c_0$ equals the period length $c_1 - c_0$, where $c_0$ and $c_1$ are the preceding and next closure points in the periodic table.
background
The module derives atomic radii from φ-ladder scaling. Period length is defined as nextClosure Z minus prevClosure Z. Valence electrons are defined as Z minus prevClosure Z. The Recognition Science insight is that noble gases occur precisely where these two quantities coincide, marking closed shells. This local setting follows the module's statement that radii decrease across a period and increase down a group, with noble gases producing local maxima due to shell completion.
proof idea
The proof is a one-line native_decide that reduces valenceElectrons 118 and periodLength 118 to integer subtraction on the closure functions and checks numerical equality by direct computation.
why it matters
The declaration verifies the full-shell endpoint for Z=118 in the RS periodic table model. It supports the shell-number scaling used for radius predictions in the Chemistry.AtomicRadii module. No downstream uses are recorded yet; the result closes the explicit check for the heaviest noble gas under the valence-equals-period-length rule.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.