alpha_over_sigma_pos
plain-language theorem explainer
The theorem shows that the ratio of the strong coupling constant to the string tension is strictly positive. Nuclear modelers deriving semi-empirical mass formula coefficients from QCD parameters would cite it to guarantee positive volume and surface contributions. The proof is a one-line term application of division positivity to the two upstream positivity results.
Claim. $0 < α_s / σ$, where $α_s = 2/17$ is the strong coupling constant from Recognition Science and $σ = φ^{-5}$ is the string tension.
background
The QCD-to-Nuclear Bridge module converts Recognition Science strong-force parameters into inputs for the semi-empirical mass formula. The constant α_strong is defined as the geometric value 2/17. The string tension is defined as φ raised to the power -5. Upstream results establish separate positivity: alpha_strong_pos unfolds the definition and applies norm_num, while stringTension_pos applies zpow_pos to phi_pos. The module states that all theorems are machine-verified with zero axioms.
proof idea
The proof is a one-line term-mode wrapper that applies the lemma div_pos directly to alpha_strong_pos and stringTension_pos.
why it matters
This positivity check is required before the ratio can enter the Cornell potential or the volume and surface coefficients of the semi-empirical mass formula. It inherits the string-tension positivity from the QFT confinement result and the coupling value from the wallpaper-group derivation of α_s. Within the Recognition Science chain it supplies a verified positivity fact between the T5 J-uniqueness step and the nuclear mass ladder.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.