neon_full_shell
plain-language theorem explainer
The declaration verifies that neon at Z=10 completes its valence shell by equating valence electron count to period length. Chemists applying Recognition Science to atomic structure would cite it to confirm closed-shell stability under φ-ladder scaling. The verification reduces to a native decision procedure that evaluates the underlying closure definitions directly.
Claim. For atomic number $Z=10$, the valence electron count $Z - p(Z)$ equals the period length $n(Z) - p(Z)$, where $p(Z)$ denotes the atomic number of the preceding noble gas closure and $n(Z)$ the next closure.
background
In the Recognition Science model of atomic radii, shell structure follows φ-ladder scaling with base radius proportional to φ raised to shell number. Period length for element Z is nextClosure Z minus prevClosure Z. Valence electrons for Z is Z minus prevClosure Z, counting electrons past the prior noble gas core. The module states that noble gases occur exactly where valence equals period length, marking complete shells. This matches the upstream doc-comment: noble gases are exactly those where valence = period length. The setting predicts radii decrease across periods from rising Z and increase down groups from new shells.
proof idea
The proof is a one-line wrapper that applies native_decide to evaluate the equality valenceElectrons 10 = periodLength 10 by direct computation on the closure functions.
why it matters
This declaration instantiates the RS insight on noble gas shell closure from the module documentation on atomic radii from φ-ladder scaling. It anchors predictions of local maxima in radii for noble gases within periods. No downstream theorems reference it yet, but it grounds the chemistry module's treatment of shell trends and connects to φ-based coherence length scaling in the broader framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.