solvationShellCert
plain-language theorem explainer
The definition constructs the canonical witness for the SolvationShellCert structure, asserting exactly five shells with consecutive radii in golden ratio and all radii positive. Solvation chemists or modelers of ionic hydration layers would cite the certificate when invoking the D=5 phi-ladder configuration. It is assembled by direct structure construction from the cardinality, ratio, and positivity results.
Claim. Let SolvationShellCert be the structure whose fields require that the number of solvation shells equals five, that consecutive shell radii satisfy $r(k+1)/r(k) = phi$ for all $k$, and that every shell radius is strictly positive. The definition supplies the unique term witnessing this structure.
background
The module models five canonical solvation shells for an ionic solute in water when configDim equals 5: primary hydration, secondary hydration, tertiary hydration, bulk-boundary layer, and far bulk. Shell radii lie on the phi-ladder with adjacent ratio exactly phi. The structure SolvationShellCert packages these three requirements into a single certificate object.
proof idea
The definition is a one-line structure constructor that supplies the three fields directly: five_shells from solvationShell_count, phi_ratio from shellRadius_ratio, and radius_always_pos from shellRadius_pos.
why it matters
This definition closes the local development by exhibiting the concrete witness for the five-shell phi-ladder configuration required by any Recognition Science chemistry model. It draws the cardinality, ratio, and positivity lemmas from the same module and the phi_ratio constant from the Quasicrystal import, aligning with the phi-ladder and configDim = D = 5 setting of the B10 Chemistry Depth section.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.