module module high

`IndisputableMonolith.Chemistry.AtomicRadii`

AtomicRadii module supplies shellNumber and radius proxies for phi-ladder atomic scaling in Recognition Science chemistry. Researchers modeling atomic properties via eight-tick octave structure without per-element tuning would cite it. The module consists of definitions and supporting lemmas atop PeriodicTable imports.

claimThe module defines the 1-indexed shell number function $n(Z)$ for atomic number $Z$ together with shell radius proxy, screening factor, and normalized radius functions that scale atomic radii on the $\phi$-ladder.

background

This module sits in the Chemistry domain and imports PeriodicTable, whose doc states it supplies an 'Octave ↔ eight-tick mapping for chemistry: φ-tier rails with a fixed set of block offsets (s/p/d/f) and an eight-window neutrality predicate' together with a 'minimal, zero-parameter API surface'. It also imports Constants, whose doc identifies the RS time quantum $ au_0 = 1$ tick. The module DOC_COMMENT specifies that shellNumber is 1-indexed for atomic radii scaling.

proof idea

this is a definition module, no proofs

why it matters in Recognition Science

The module feeds the Electronegativity module whose doc describes 'Electronegativity from φ-Ladder Scaling (CH-008)' and states that 'RS mechanism: EN ~ distToNextClosure^(-1) modulated by shell number'. It supplies the shell structure component required for downstream electronegativity and radius predictions inside the eight-tick framework.

scope and limits

Does not compute numerical radii from experimental datasets.
Does not introduce element-specific fitting parameters.
Does not prove direct links to physical constants beyond imported modules.
Does not address relativistic corrections or many-body effects.

used by (1)

From the project-wide theorem graph. These declarations reference this one in their body.

IndisputableMonolith.Chemistry.Electronegativity module_import

depends on (2)

Lean names referenced from this declaration's body.

IndisputableMonolith.Chemistry.PeriodicTable module_import
IndisputableMonolith.Constants module_import

declarations in this module (28)

def shellNumber L33
def shellRadiusProxy L37
def screeningFactor L42
def radiusProxy L48
def normalizedRadius L53
theorem lower_z_more_remaining L63
theorem shell_radius_increases_with_period L75
theorem li_valence_one L87
theorem na_valence_one L88
theorem k_valence_one L89
theorem rb_valence_one L90
theorem cs_valence_one L91
theorem fr_valence_one L92
theorem f_dist_one L95
theorem cl_dist_one L96
theorem br_dist_one L97
theorem i_dist_one L98
theorem at_dist_one L99
theorem helium_full_shell L102
theorem neon_full_shell L103
theorem argon_full_shell L104
theorem krypton_full_shell L105
theorem xenon_full_shell L106
theorem radon_full_shell L107
theorem oganesson_full_shell L108
theorem li_larger_than_f L115
theorem na_larger_than_cl L122
theorem k_larger_shell_than_li L127