SolvationShellCert
SolvationShellCert defines a record certifying five solvation shells for an ionic solute in water whose radii form a geometric sequence with common ratio the golden ratio φ. Chemists applying the Recognition framework to hydration layers cite it when placing shells on the φ-ladder. The structure is a direct record whose three fields are satisfied by the cardinality of a five-element inductive type, the ratio property of the exponential radius function, and positivity of all powers of φ.
claimLet $S$ be the inductive type whose five constructors are primary hydration, secondary hydration, tertiary hydration, bulk-boundary layer and far bulk. The certification structure asserts that the cardinality of $S$ equals 5, that the shell radius function $r(k) = φ^k$ satisfies $r(k+1)/r(k) = φ$ for every natural number $k$, and that $r(k) > 0$ for all $k$.
background
The module treats solvation shells for an ionic solute in water when the configuration dimension equals 5. It introduces the inductive type whose constructors label the five canonical layers: primary hydration, secondary hydration, tertiary hydration, bulk-boundary layer and far bulk. The radius function is defined by $r(k) = φ^k$, so that adjacent shells differ by the fixed factor φ on the ladder.
proof idea
The declaration is a structure definition whose fields are the three required properties. The downstream definition solvationShellCert populates them by applying the cardinality lemma for the five-constructor inductive type, the ratio identity for the exponential shellRadius function, and the positivity of positive powers of φ.
why it matters in Recognition Science
The structure is instantiated by solvationShellCert and supplies the certificate for the five-shell model in the B10 Chemistry Depth. It realizes the φ-ladder in a concrete chemical setting, consistent with the self-similar fixed point forced at T6 and the Recognition Composition Law. The construction bridges the abstract forcing chain to solvation radii while preserving the RS-native constants expressed in powers of φ.
scope and limits
- Does not derive shell existence from quantum mechanics.
- Does not compute numerical radii for specific ions.
- Does not treat non-aqueous solvents.
- Does not vary the number of shells with configDim.
formal statement (Lean)
40structure SolvationShellCert where
41 five_shells : Fintype.card SolvationShell = 5
42 phi_ratio : ∀ k, shellRadius (k + 1) / shellRadius k = phi
43 radius_always_pos : ∀ k, 0 < shellRadius k
44