SolvationShellCert
plain-language theorem explainer
SolvationShellCert packages the assertion of exactly five solvation shells whose radii form a geometric sequence of common ratio phi with all radii positive. Chemists modeling ionic hydration inside the Recognition Science framework cite it to link configDim D=5 to the five-layer hydration structure. The declaration is a plain structure definition whose three fields directly record the required properties with no additional obligations.
Claim. A record type whose fields assert that the set of solvation shells has cardinality 5, that consecutive shell radii satisfy the ratio equal to the golden ratio for every index, and that every shell radius is strictly positive.
background
The module treats five canonical solvation shells for an ionic solute in water when the configuration dimension equals 5. These shells are primary hydration, secondary hydration, tertiary hydration, bulk-boundary layer, and far bulk, introduced as the inductive type with five constructors and deriving Fintype. Shell radii are supplied by the definition shellRadius k := phi^k, placing successive shells on the phi-ladder with adjacent ratio phi. The upstream phi_ratio definition from Quasicrystal supplies the inverse golden ratio from Constants, while the local setting in the module doc states that Lean status is zero sorry and zero axiom.
proof idea
The declaration is a structure definition that introduces a record type whose three fields reference the inductive SolvationShell, the definition shellRadius, and the constant phi. No lemmas are invoked and no tactics are applied.
why it matters
SolvationShellCert supplies the type instantiated by the downstream solvationShellCert construction, which assembles the concrete certificate from the lemmas solvationShell_count, shellRadius_ratio, and shellRadius_pos. It realizes the B10 chemistry depth by embedding the five-shell model from configDim D=5 onto the phi-ladder, consistent with the forcing chain landmarks of T7 eight-tick octave and D=3 spatial dimensions. No open questions are addressed.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.