k_larger_shell_than_li
plain-language theorem explainer
Potassium (Z=19) receives a strictly larger shell index than lithium (Z=3) under the Recognition Science phi-ladder assignment of atomic shells. Modelers of periodic radius trends cite the ordering to ground the group-wise increase in effective radius. The verification reduces to direct numerical evaluation of the shell function on the two concrete atomic numbers.
Claim. The shell index assigned to potassium exceeds the shell index assigned to lithium: $n(19) > n(3)$, where $n(Z)$ equals the period index of $Z$ plus one and the period index scales as a power of the golden ratio.
background
Atomic radii in the Recognition Science framework are derived from phi-ladder scaling of shell structure. The shell index for an element with atomic number $Z$ is obtained by adding one to its period index, with the period index itself given by a power of the golden ratio. This produces the base radius scaling before screening corrections are applied. The module sets out three empirical trends: radii decrease across a period as nuclear charge increases, radii increase down a group as new shells appear farther from the nucleus, and d/f-block filling produces contraction. Upstream results supply the period function as a direct power of the golden ratio and the shell index definition that adds one to the period index.
proof idea
The proof is a one-line wrapper that applies native_decide to evaluate the concrete inequality on the two atomic numbers.
why it matters
The result anchors the group trend in the atomic-radii module, confirming that alkali metals occupy successively higher shells and therefore exhibit larger base radii. It supplies a concrete instance of the phi-ladder shell assignment used throughout the chemistry section. No downstream theorems are recorded, so the declaration functions as a verified building block rather than an intermediate lemma. It touches the open question of how screening factors modulate the raw phi-power radii once the shell ordering is fixed.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.