normalizedRadius
plain-language theorem explainer
The normalizedRadius definition supplies a position-based scaling for atomic radii within each periodic table period, mapping atomic number Z from the previous to next noble-gas closure onto the unit interval with inversion so higher Z yields smaller values. Atomic physicists modeling RS shell structure would cite it when deriving period trends or comparing radii across elements such as alkali metals versus halogens. The definition is a direct piecewise linear interpolation using the prevClosure and nextClosure functions from the PeriodicTable.
Claim. Let $p(Z)$ and $n(Z)$ denote the previous and next noble-gas closures for atomic number $Z$. The normalized radius is $r(Z) = 1$ if $n(Z) = p(Z)$, otherwise $r(Z) = 1 - (Z - p(Z))/(n(Z) - p(Z))$.
background
In the Recognition Science treatment of chemistry, atomic radii follow shell structure with base scaling by shell number on the φ-ladder and effective reduction from valence-electron screening. The module states that radii decrease across a period as increasing Z pulls electrons closer and increase down a group with new shells farther from the nucleus. The functions prevClosure and nextClosure identify the bounding noble-gas configurations for each Z, returning the prior closed shell (0 for Z ≤ 2) or next closed shell (2, 10, 18, 36, 54, …) respectively.
proof idea
This is a direct definition that first evaluates prevClosure Z and nextClosure Z, then returns 1 on equality or else performs the arithmetic 1 minus the normalized offset of Z inside the interval. It applies only the closure functions from PeriodicTable and executes a simple conditional reduction with no external lemmas.
why it matters
This definition underpins the explicit comparisons in li_larger_than_f and na_larger_than_cl, which verify that Li exceeds F and Na exceeds Cl in normalized radius, matching the RS period-contraction prediction. It fills the CH-007 claim for intra-period normalization on which φ-ladder radii are later built. The construction directly encodes the module's stated mechanism that radii contract toward the next closure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.