pith. machine review for the scientific record. sign in
def definition def or abbrev high

solvationShellCert

show as:
view Lean formalization →

The solvationShellCert definition supplies a concrete instance of the SolvationShellCert structure for five hydration shells around an ionic solute. Researchers in physical chemistry modeling water structure would cite it when invoking the phi-scaled radii. The construction proceeds by direct field assignment from the shell count theorem and the two radius lemmas.

claimLet SolvationShellCert be the structure asserting that the number of solvation shells equals five, that consecutive shell radii satisfy $r_{k+1}/r_k = phi$ for all $k$, and that each radius is positive. The definition realizes this structure by substituting the theorem that the cardinality equals five, the theorem that the ratio equals $phi$, and the theorem that all radii are positive.

background

In the Recognition Science treatment of chemistry, solvation shells are modeled for an ionic solute in water when the configuration dimension is five. This yields five canonical layers: primary hydration, secondary hydration, tertiary hydration, bulk-boundary layer, and far bulk. Shell radii lie on the phi-ladder with adjacent shells in ratio phi. The SolvationShellCert structure packages three properties: the cardinality of the SolvationShell type equals five, the ratio shellRadius(k+1)/shellRadius(k) equals phi for all k, and shellRadius(k) > 0 for all k. Upstream, the phi_ratio definition supplies the inverse golden ratio from the quasicrystal module, while shellRadius_ratio and shellRadius_pos are proved by direct computation with powers of phi.

proof idea

The definition is a direct construction of the SolvationShellCert record. It assigns the result of solvationShell_count to the five_shells field, the result of shellRadius_ratio to the phi_ratio field, and the result of shellRadius_pos to the radius_always_pos field.

why it matters in Recognition Science

This definition completes the local chemistry module by exhibiting an explicit certificate for the five-shell structure with phi-scaled radii. It draws on the phi-ladder from the quasicrystal foundation and the configDim = 5 convention for solvation. No downstream uses are recorded, indicating it serves as a terminal interface for higher-level models of ionic hydration. It aligns with the Recognition Science emphasis on self-similar scaling via phi.

scope and limits

formal statement (Lean)

  45noncomputable def solvationShellCert : SolvationShellCert where
  46  five_shells := solvationShell_count

proof body

Definition body.

  47  phi_ratio := shellRadius_ratio
  48  radius_always_pos := shellRadius_pos
  49
  50end IndisputableMonolith.Chemistry.SolvationShellsFromConfigDim

depends on (5)

Lean names referenced from this declaration's body.