li_larger_than_f
plain-language theorem explainer
Lithium has a larger normalized atomic radius than fluorine within period 2 under the Recognition Science phi-ladder scaling. Modelers of periodic trends cite the result to confirm the predicted monotonic decrease in radius with rising Z inside a shell. The proof reduces the inequality to arithmetic by unfolding the closure-based definition and normalizing the numbers.
Claim. The normalized atomic radius of lithium exceeds that of fluorine: $r(3) > r(9)$, where $r(Z) = 1 - (Z - p(Z))/(n(Z) - p(Z))$ with $p$ the previous noble-gas closure and $n$ the next, yielding $7/8 > 1/8$ for the period-2 bounds 2 and 10.
background
Atomic radii follow phi-ladder scaling with shell structure. The normalized radius function returns a value in [0,1] inside each period, equal to 1 immediately after a noble-gas closure and 0 at the next closure. It is computed from the previous and next noble-gas closures supplied by the PeriodicTable module.
proof idea
One-line wrapper that applies simp to unfold normalizedRadius together with the two closure functions, then discharges the resulting numerical comparison with norm_num.
why it matters
The theorem instantiates the CH-007 period-trend prediction that radii decrease across a period because increasing Z pulls electrons inward. It anchors the screening mechanics used in the mass-anchor and cellular-automaton radius definitions. No direct downstream theorems are recorded, leaving open the extension to d- and f-block contractions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.