module module high

`IndisputableMonolith.Chemistry.AtomicRadii`

The AtomicRadii module defines the 1-indexed shell number and associated radius proxies for atomic scaling under the phi-ladder. Downstream chemistry modules such as Electronegativity cite these definitions to modulate predictions by shell structure. The module contains only definitions and supporting lemmas with no proof obligations.

claim$n(Z)$ denotes the 1-indexed shell number for atomic number $Z$, together with the proxies shellRadiusProxy, screeningFactor, radiusProxy and normalizedRadius that scale radii on the phi-ladder.

background

The module imports the PeriodicTable engine, whose doc-comment states it supplies an octave to eight-tick mapping for chemistry via phi-tier rails, fixed s/p/d/f block offsets, and an eight-window neutrality predicate with zero per-element tuning. It also imports Constants, whose doc-comment identifies the fundamental RS time quantum tau_0 equal to one tick. These imports establish the phi-ladder and eight-tick octave setting in which shellNumber and the radius proxies operate.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

The module supplies the shell-number component required by the Electronegativity module, whose doc-comment states that electronegativity follows distToNextClosure to the minus one, modulated by shell number. It therefore implements the shell-structure layer of the eight-tick octave chemistry scaffold described in the PeriodicTable doc-comment.

scope and limits

Does not compute numerical radius values from measured data.
Does not introduce element-specific fitting constants.
Does not address relativistic corrections to radii.
Does not derive ionization energies or electron affinities.

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