shellRadius_ratio
plain-language theorem explainer
The ratio of radii for consecutive solvation shells equals the golden ratio phi. Physical chemists constructing hydration models around ions would cite this when placing shell sizes on the phi-ladder. The proof is a direct algebraic reduction that unfolds the power definition and applies exponent rules plus ring simplification.
Claim. For every natural number $k$, if the radius of shell $k$ satisfies $r(k) = phi^k$, then $r(k+1)/r(k) = phi$.
background
The module treats solvation shells for an ionic solute in water under configDim D=5, producing five layers from primary hydration to far bulk. Shell radii sit on the phi-ladder with the explicit definition that the radius of shell index k equals phi raised to k. This places adjacent shells in geometric progression with common ratio phi, consistent with the self-similar fixed point property of phi.
proof idea
The term proof first unfolds the shell radius definition to replace both terms by powers of phi. It introduces the positivity fact for phi to the k, rewrites the division equation via the division-iff lemma, replaces the successor exponent, and finishes with ring normalization.
why it matters
The result populates the phi_ratio field inside the SolvationShellCert definition that certifies the five-shell structure. It directly instantiates the forced self-similar fixed point of phi (T6) inside the chemistry domain and confirms the eight-tick octave scaling carries into solvation geometry. No open scaffolding remains for this step.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.