module module high

`IndisputableMonolith.Chemistry.AtomicRadii`

AtomicRadii supplies shell-number and radius-proxy definitions for phi-ladder scaling of atomic sizes in Recognition Science chemistry. Researchers building zero-parameter periodic-trend models would cite these functions when extending the eight-tick octave structure. The module imports PeriodicTable for block offsets and neutrality predicates plus Constants for the base tick, then defines helpers such as shellNumber and normalizedRadius. It is a pure definition module with no theorems or proofs.

claimShell number function $n(Z)$ (1-indexed) for atomic number $Z$, together with radius proxy $r(Z) = f(n(Z), s(Z))$ where $s(Z)$ is a screening factor, and normalized radius $r_n(Z)$ for use in phi-ladder atomic-size calculations.

background

Recognition Science maps chemistry onto an eight-tick octave via the PeriodicTable module, which supplies φ-tier rails, fixed s/p/d/f block offsets, and an eight-window neutrality predicate that detects noble-gas closures. The AtomicRadii module introduces shellNumber as the 1-indexed shell index for radii scaling, along with shellRadiusProxy, screeningFactor, radiusProxy, and normalizedRadius to produce effective sizes without per-element tuning. Constants anchors the construction with the fundamental time quantum τ₀ = 1 tick.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

AtomicRadii supplies the shell-structure component required by the Electronegativity module (CH-008), whose doc-comment states that electronegativity follows distToNextClosure^{-1} modulated by shell number. It completes the phi-ladder input layer for chemistry, allowing the upstream PeriodicTable octave mapping to propagate into concrete atomic-property predictions without empirical fitting.

scope and limits

Does not compute numerical values from experimental radius datasets.
Does not incorporate relativistic effects for high-Z elements.
Does not define electronegativity or ionization energies.
Does not extend the eight-window neutrality predicate beyond PeriodicTable.
Does not treat molecular or bonding radii.

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