shellRadius_pos
plain-language theorem explainer
The theorem shows that shell radius at any natural-number level k is strictly positive. Modelers of ionic hydration layers cite it to ensure all five shells on the phi-ladder have positive radii. The proof is a one-line wrapper applying the standard positivity-of-powers lemma to the positivity of phi.
Claim. For every natural number $k$, the $k$-th solvation-shell radius $r_k = phi^k$ satisfies $r_k > 0$.
background
The module defines five canonical solvation shells for an ionic solute in water (configDim D=5): primary hydration, secondary hydration, tertiary hydration, bulk-boundary layer, and far bulk. Shell radii follow the phi-ladder with adjacent-shell ratio exactly phi. The upstream definition states that shell radius at level k equals phi raised to k, where phi is the self-similar fixed point from the forcing chain.
proof idea
One-line wrapper that applies the lemma pow_pos to the known positivity of phi and the index k.
why it matters
This supplies the radius_always_pos field inside solvationShellCert, which certifies the five-shell model. It anchors the B10 chemistry depth to the phi-ladder and the eight-tick octave of Recognition Science, guaranteeing positivity without extra hypotheses.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.