stringTension_pos
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 in Recognition Science
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.
scope and limits
- Does not compute a numerical value of string tension in fm units.
- Does not derive the exponent -5 from QCD dynamics.
- Does not address temperature or density corrections to the tension.
formal statement (Lean)
42theorem stringTension_pos : 0 < stringTension := by
proof body
Term-mode proof.
43 unfold stringTension
44 exact zpow_pos phi_pos _
45
46/-- φ^5 is between 10 and 12 (using bounds on φ). -/