screeningFactor
plain-language theorem explainer
The screeningFactor definition supplies a multiplicative correction to atomic radii that decreases linearly with the fraction of valence electrons within each period. Chemists or RS modelers working on predicted atomic sizes would cite it when scaling shell radii for screening penetration. It is implemented as a direct conditional expression that returns 1 for zero-length periods and otherwise subtracts the normalized valence count from 1.
Claim. Let $s(Z)$ be the screening factor for atomic number $Z$. Then $s(Z) = 1$ whenever the period length $p(Z)$ containing $Z$ is zero, and $s(Z) = 1 - v(Z)/(2 p(Z))$ otherwise, where $v(Z)$ counts the valence electrons beyond the previous noble-gas core and $p(Z)$ is the number of elements in the period.
background
The AtomicRadii module implements CH-007 predictions that atomic radii follow phi-ladder scaling with shell number: base radius proportional to phi^k for shell index k, decreasing across a period from rising nuclear charge and increasing down a group with added shells. The screening factor supplies the explicit reduction in effective radius as valence electrons increase, matching the module statement that radius scales as shellRadius times (1 minus valence over period length).
proof idea
This is a direct definition. It applies the upstream periodLength and valenceElectrons functions in a single conditional expression: return 1 if periodLength Z equals zero, otherwise compute 1 minus (valenceElectrons Z cast to real) divided by twice (periodLength Z cast to real). No additional lemmas or tactics are invoked.
why it matters
screeningFactor is multiplied by shellRadiusProxy inside the radiusProxy definition, which produces the final atomic-radius proxy used for period and group trend checks. It directly encodes the RS mechanism of valence screening on the phi-ladder, supporting the module's claims about noble-gas maxima, alkali-metal maxima, and halogen minima. The construction remains consistent with the eight-tick octave and D=3 spatial structure of the broader framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.