Pith. sign in
module module moderate

IndisputableMonolith.Chemistry.VanDerWaals

show as:
view Lean formalization →

Fit-free chemistry scaffold for noble-gas Van der Waals trends in Recognition Science. It records noble-gas Z values, boiling-point data, polarizability and London-dispersion proxies, a Lennard-Jones potential with an approximate minimum, and the He→Rn boiling-point chain. Auditors checking residual attractions after noble-gas shell closure would cite it. Most content is definitions plus elementary numeric inequalities.

claimNoble-gas atomic numbers and boiling points; polarizability and London-dispersion proxies; Lennard-Jones potential $V_{\mathrm{LJ}}(r)$ with approximate minimizing distance; and the ordering $T_b(\mathrm{He})<T_b(\mathrm{Ne})<T_b(\mathrm{Ar})<T_b(\mathrm{Kr})<T_b(\mathrm{Xe})<T_b(\mathrm{Rn})$.

background

Recognition Science chemistry sits on the Periodic Table engine: an octave / eight-tick map with $\varphi$-tier rails, fixed $s/p/d/f$ block offsets, and an eight-window neutrality predicate that marks noble-gas shell closures as "rests." No per-element tuning is allowed; the API is deliberately zero-parameter so downstream predictions stay falsifiable.

After a closed shell, residual cohesion is Van der Waals attraction, dominated for noble gases by London dispersion. This module packages the minimal objects needed to state that residual: a noble-gas list, boiling-point anchors, scalar proxies for polarizability and dispersion strength, and a standard Lennard-Jones pair potential whose minimum sets a characteristic length.

Constants enter only through the shared RS tick $\tau_0=1$; the chemistry layer does not rebind $c$, $\hbar$, or $G$ here.

proof idea

Primarily a definition module. Noble-gas sets, boiling-point tables, polarizability/dispersion proxies, and the Lennard-Jones form are introduced as data or closed-form defs. The proved content is a short chain of elementary comparisons: each consecutive noble-gas boiling-point inequality (He–Ne, Ne–Ar, Ar–Kr, Kr–Xe, Xe–Rn) is a direct numeric check. The LJ minimum lemma is an approximate algebraic location of the potential well, not a deep existence proof.

why it matters in Recognition Science

Closes the residual-force side of noble-gas "rests" from the Periodic Table engine: once eight-window neutrality marks a closed shell, this module supplies the language for weak cohesion that still rises with size and polarizability. That matches the qualitative He→Rn boiling-point ladder without dataset binding.

No downstream theorems currently import it (leaf scaffold). It is the natural hook for later chemistry falsifiers: predicted ordering or scaling of dispersion proxies against $\varphi$-tier rails, or LJ length scales tied to the eight-tick octave. It does not yet touch mass-ladder rungs or the $\alpha$ band; those remain separate RS landmarks.

scope and limits

depends on (2)

Lean names referenced from this declaration's body.

declarations in this module (16)