na_larger_than_cl
plain-language theorem explainer
Normalized atomic radius for sodium (Z=11) exceeds that for chlorine (Z=17) inside period 3. Chemists checking RS predictions for intra-period size trends cite the result to confirm the linear screening model. The proof is a one-line wrapper that unfolds normalizedRadius with the closure functions and reduces the comparison to arithmetic.
Claim. Let $r(Z)$ denote the normalized atomic radius of element $Z$, defined by $r(Z) = 1 - (Z - p(Z))/(n(Z) - p(Z))$ where $p(Z)$ is the previous noble-gas closure and $n(Z)$ the next closure. Then $r(11) > r(17)$.
background
Normalized atomic radius maps each element to a value in [0,1] inside its period, with 0 at the smallest radius and 1 at the largest; it is computed from the fractional distance between the preceding and following noble-gas closures. prevClosure(Z) returns the atomic number of the last closed shell before Z, while nextClosure(Z) returns the atomic number of the next closed shell after Z. The module places these radii inside the φ-ladder scaling of CH-007, where effective radius decreases across a period because increasing nuclear charge pulls electrons inward while the shell capacity remains fixed.
proof idea
The term proof applies simp only on the definitions of normalizedRadius, prevClosure and nextClosure, then invokes norm_num to evaluate the concrete fractions 7/8 and 1/8 and discharge the inequality.
why it matters
The declaration fills the period-trend prediction of the RS chemistry module (CH-007), showing that the normalized-radius construction reproduces the expected monotonic decrease within a shell. It supplies a concrete check on the linear interpolation between closures that later mass and spectroscopy lemmas rely upon. No open scaffolding remains for this specific comparison.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.