shellRadiusProxy
Shell radius proxy sets the base atomic radius for element Z as phi raised to the shell number. Recognition Science chemists cite it when deriving period and group trends in atomic sizes from the phi-ladder. The definition is a direct one-line exponentiation using the shell index computed upstream from the periodic table structure.
claimFor atomic number $Z$, the raw shell radius proxy equals $phi^{n(Z)}$ where $n(Z)$ is the shell number (period index plus one).
background
The module Atomic Radii from φ-Ladder Scaling (CH-007) models atomic radii via coherence length on the phi-ladder. Base radius scales as phi to the shell number; effective radius then decreases with valence electrons via screening. Period trends arise because higher Z pulls electrons inward while new shells down a group increase the base radius.
proof idea
One-line definition that applies the exponential phi scaling directly to the shell number for Z, reusing the upstream shellNumber definition.
why it matters in Recognition Science
Supplies the base term for the downstream radiusProxy definition, which multiplies by screeningFactor to produce the composite atomic radius. It realizes the CH-007 claim that radii follow phi^n with n the shell index and feeds the group-maxima predictions for alkali metals after noble-gas closures. The scaling inherits from the T6 phi fixed point and the phi-ladder mass formula in the forcing chain.
scope and limits
- Does not include screening or valence penetration effects.
- Does not output radii in physical units or angstroms.
- Applies only to the integer-Z proxy scaling, not full electronic structure.
- Assumes the upstream shellNumber definition without re-deriving periods.
Lean usage
def radiusProxy (Z : ℕ) : ℝ := shellRadiusProxy Z * screeningFactor Zformal statement (Lean)
37def shellRadiusProxy (Z : ℕ) : ℝ :=
proof body
Definition body.
38 Constants.phi ^ (shellNumber Z : ℝ)
39
40/-- Screening factor: valence electrons penetrate less as they increase.
41 radius ~ shellRadius * (1 - valence/periodLength) -/