r_min_pos
plain-language theorem explainer
r_min_pos establishes that the nuclear saturation radius is strictly positive. Modelers of nuclear binding energies via the semi-empirical mass formula cite it to keep radius-dependent terms physically consistent. The proof is a one-line term application of square-root positivity to the ratio of two already-positive constants.
Claim. $0 < r_min$ where $r_min := sqrt(alpha_s / sigma)$ with $alpha_s > 0$ the strong coupling constant and $sigma > 0$ the string tension.
background
The QCD-to-Nuclear Bridge module parameterizes the strong force at the QCD level with alpha_strong (derived from wallpaper groups as 2/17) and stringTension (equal to phi^{-5} in RS units). The nuclear saturation radius is introduced by the definition r_min = sqrt(alpha_strong / stringTension). Upstream theorems alpha_strong_pos and stringTension_pos already establish that both quantities are positive.
proof idea
The proof is a term-mode one-liner that applies Real.sqrt_pos_of_pos directly to the result of div_pos alpha_strong_pos stringTension_pos. No additional tactics or lemmas are required beyond the positivity of the ratio and the square-root function.
why it matters
The result closes a basic consistency requirement for the saturation radius that enters the Cornell potential and the volume/surface coefficients of the semi-empirical mass formula. It therefore supports the module's overall bridge from Recognition Science constants (phi-ladder, T5 J-uniqueness) to nuclear scales. No downstream theorems yet depend on it.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.