shellRadius_pos
plain-language theorem explainer
The theorem shows that the radius of the k-th solvation shell is strictly positive for every natural number k. Chemists constructing hydration models around ions cite it to guarantee that all five shells on the phi-ladder have positive extent. The proof is a one-line application of the standard lemma that positive bases raised to any power remain positive.
Claim. For every natural number $k$, if $r(k) = phi^k$ then $r(k) > 0$.
background
The module defines five canonical solvation shells for an ionic solute in water when configDim equals 5: primary hydration, secondary hydration, tertiary hydration, bulk-boundary layer, and far bulk. Shell radii lie on the phi-ladder with adjacent-shell ratio exactly phi. The upstream definition states noncomputable def shellRadius (k : ℕ) : ℝ := phi ^ k, so the positivity claim applies directly to these radii.
proof idea
One-line wrapper that applies pow_pos to phi_pos.
why it matters
The result supplies the radius_always_pos field inside the SolvationShellCert record, which also records the shell count and the phi ratio. It closes the chemistry depth B10 construction by ensuring the phi-ladder radii remain physically admissible. The module states zero sorry and zero axiom for the entire solvation-shell package.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.