solvationShell_count
plain-language theorem explainer
The theorem fixes the cardinality of the solvation-shell type at five for an ionic solute in water under configuration dimension five. Modelers in Recognition Science chemistry cite the result to anchor the discrete shell count before deriving radius ratios on the phi-ladder. The proof is a one-line decision procedure that counts the five explicit inductive constructors.
Claim. The finite type of solvation shells has cardinality five: $ |SolvationShell| = 5 $.
background
The module defines five canonical solvation shells for an ionic solute in water when configDim equals five: primary hydration, secondary hydration, tertiary hydration, bulk-boundary layer, and far bulk. Adjacent shells sit on the phi-ladder with radius ratio phi. The upstream inductive definition enumerates exactly these five cases and derives the Fintype instance used by the cardinality statement.
proof idea
The proof is a one-line wrapper that applies the decide tactic directly to Fintype.card SolvationShell = 5. The tactic succeeds because the inductive type carries DecidableEq and the enumeration is finite and explicit.
why it matters
The result supplies the five_shells field inside the downstream solvationShellCert definition. It completes the B10 chemistry depth by locking the shell count to configDim D = 5 and the phi-ladder geometry. The construction sits inside the Recognition Science forcing chain after T8 and before radius-ratio derivations.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.