stringTension_pos
plain-language theorem explainer
String tension equals φ to the power of negative five in Recognition Science units. Nuclear modelers cite this result when establishing that α_s/σ exceeds one or that the minimum radius r_min is positive. The proof is a one-line term that unfolds the definition and applies positivity of real powers for a positive base.
Claim. $0 < σ$ where $σ := φ^{-5}$ and $φ > 0$ is the golden-ratio fixed point.
background
The QCD-to-Nuclear Bridge module introduces string tension as σ = φ^{-5} to link the strong coupling α_s = 2/17 (from wallpaper groups) to semi-empirical mass formula coefficients. The sibling definition stringTension supplies the explicit expression σ = Constants.phi ^ (-(5:ℤ)). Upstream results include the general lemma that a positive base raised to any integer power remains positive, together with the positivity of φ itself.
proof idea
The term proof unfolds stringTension to φ^{-5} and applies the lemma zpow_pos instantiated at phi_pos.
why it matters
This positivity feeds the three immediate downstream theorems alpha_over_sigma_pos, alpha_over_sigma_gt_one, and r_min_pos inside the same module. It supplies the basic sign check required before comparing strong coupling to string tension and before extracting the nuclear radius parameter. The result sits inside the framework's assignment of string tension to φ^{-5} in RS-native units.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.