shellRadius_ratio
plain-language theorem explainer
Consecutive solvation shell radii stand in the constant ratio phi when each radius is defined as a power of phi. Chemists constructing hydration models for ionic solutes cite the result to confirm geometric progression across the five canonical shells. The term-mode proof unfolds the power definition, invokes positivity of phi to the k, rewrites via division equivalence and successor expansion, then normalizes with ring.
Claim. For every natural number $k$, the ratio of the radius of the $(k+1)$-th solvation shell to the radius of the $k$-th solvation shell equals the golden ratio $phi$, where the radius of shell level $k$ is $phi^k$.
background
The module treats solvation shells for an ionic solute in water with configDim equal to 5, producing five shells: primary hydration, secondary hydration, tertiary hydration, bulk-boundary layer, and far bulk. Radii lie on the phi-ladder so adjacent shells differ by the factor phi. The upstream definition states that the radius of shell $k$ equals $phi$ raised to the power $k$.
proof idea
Unfold the shell radius definition to obtain $phi^{k+1}/phi^k$. Introduce the positivity hypothesis $0 < phi^k$ via the pow_pos lemma. Rewrite the division using div_eq_iff, expand the numerator with pow_succ, and finish by ring normalization.
why it matters
The theorem supplies the phi_ratio field inside the SolvationShellCert record that certifies the five-shell configuration. It encodes the adjacent-shell ratio property stated in the module documentation for B10 Chemistry Depth. In the Recognition framework it instantiates self-similar scaling on the phi-ladder at the chemistry level.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.