shellRadius_pos
plain-language theorem explainer
The theorem shows that every solvation-shell radius defined by phi to the power k remains strictly positive for natural k. Modelers of ionic hydration layers cite it to confirm that all five shells (primary through far bulk) have positive extent on the phi-ladder. The proof is a one-line wrapper applying the power-positivity lemma to the established 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 treats solvation shells for an ionic solute in water under configDim = 5, producing five canonical layers whose radii lie on the phi-ladder with adjacent ratio phi. The upstream definition supplies the explicit form shell radius at level k equals phi to the power k. The module header records zero sorry and zero axiom for the entire development.
proof idea
One-line wrapper that applies the lemma pow_pos to the positivity of phi.
why it matters
The result populates the radius_always_pos field of the solvationShellCert definition, which assembles the five-shell count, the phi ratio, and the positivity guarantee. It supplies a concrete link from the phi-ladder (T6) to B10 Chemistry Depth. No open questions are noted in the supplied material.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.