SolvationShellCert
plain-language theorem explainer
SolvationShellCert packages three properties into a record type: exactly five solvation shells, consecutive radii in geometric progression with ratio phi, and all radii positive. Modelers of ionic hydration in the Recognition Science framework cite it to certify the phi-ladder structure when configDim equals 5. The declaration is a pure structure definition carrying no proof obligations or computational content.
Claim. A record type whose fields assert that the set of solvation shells has cardinality 5, that shellRadius$(k+1)$/shellRadius$(k)$ equals the golden ratio phi for every natural number $k$, and that shellRadius$(k)>0$ for every $k$.
background
The module treats an ionic solute in water when the configuration dimension equals 5. It enumerates five shells via the inductive type SolvationShell whose constructors are primaryHydration, secondaryHydration, tertiaryHydration, bulkBoundary and farBulk; this type derives Fintype so that its cardinality is well-defined. Shell radii sit on the phi-ladder by the definition shellRadius$(k)$ := phi$^k$. The upstream constant phi_ratio supplies the inverse golden ratio as a convex energy proxy.
proof idea
The declaration is a structure definition with an empty proof body. It simply declares the three fields that any certificate must satisfy; no lemmas are applied and no tactics are used.
why it matters
The structure is instantiated downstream by solvationShellCert, which supplies the concrete witnesses five_shells, phi_ratio and radius_always_pos. It encodes the B10 Chemistry Depth claim that five phi-scaled shells arise directly from configDim = 5 and the phi-ladder, connecting to the Recognition Science constants and the eight-tick octave. No open scaffolding questions are attached.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.