Pith. sign in
module module moderate

IndisputableMonolith.Chemistry.SolvationShellsFromConfigDim

show as:
view Lean formalization →

Chemistry module that packages solvation-shell data forced by configuration dimension: a shell type, a count, a radius map, the successive-radius ratio, positivity, and a small certificate bundle. Aimed at RS chemistry constructions that need discrete shell geometry rather than continuum solvent PDEs. Content is mostly definitions plus elementary ratio/positivity facts.

claimDiscrete solvation shells arising from configuration dimension: a shell object, a shell count, a radius function $r$, the successive ratio $r_{n+1}/r_n$, a positivity statement $r>0$, and a certificate packaging those facts.

background

Recognition Science treats chemistry geometry as forced by the same discrete configuration data that fix $D=3$ (T8) and the eight-tick octave, not by continuum electrostatics alone. This module lives in the Chemistry domain and imports only Mathlib plus Constants (where the RS time quantum satisfies $\tau_0=1$ tick).

Sibling names indicate the local vocabulary: a SolvationShell carrier, a count of shells, a radius assignment, the ratio of successive radii, a positivity lemma for those radii, and a thin certificate type that bundles the shell facts for downstream use. No continuum permittivity or radial Schrödinger equation appears here; the radii are treated as RS-native geometric data.

proof idea

Definition module. It introduces the shell carrier, count, radius map, and certificate, then records elementary consequences (successive-radius ratio and positivity). No multi-step forcing argument or deep theorem is present; supporting lemmas are short algebraic or order facts on the radius data.

why it matters in Recognition Science

Supplies the discrete shell vocabulary for the RS chemistry layer so later mass, binding, or solvent-structure results can cite a single certified shell object rather than ad-hoc radius lists. Downstream use list is currently empty, so the module is infrastructural: it closes a naming and certificate gap rather than discharging a named paper proposition. Ties conceptually to configuration dimension (T8, $D=3$) and to phi-ladder scaling used elsewhere for lengths, without re-proving those landmarks.

scope and limits

depends on (1)

Lean names referenced from this declaration's body.

declarations in this module (7)