alpha_strong_pos
The theorem proves that the Recognition Science strong coupling constant alpha_strong is strictly positive. Nuclear physicists deriving bounds on the semi-empirical mass formula coefficients cite this result to guarantee positivity of derived quantities such as r_min and alpha_over_sigma. The proof is a one-line wrapper that unfolds the definition to the rational 2/17 and applies norm_num.
claim$0 < 2/17$ where $2/17$ is the geometric strong coupling constant obtained from the wallpaper fraction in the Recognition Science framework.
background
This theorem lives in the QCD-to-Nuclear Bridge module, which connects the strong-force parameters (alpha_s = 2/17 from wallpaper groups, string tension sigma = phi^{-5}) to the coefficients of the semi-empirical mass formula. The definition alpha_strong simply casts the rational alpha_s_geom into the reals. Upstream results supply the geometric definition alpha_s_geom := 2/17 from the StrongForce module and the alias alpha_strong itself.
proof idea
The proof is a one-line wrapper: unfold alpha_strong alpha_s_geom followed by norm_num, which reduces the claim directly to the elementary inequality 0 < 2/17.
why it matters in Recognition Science
The result is invoked by the downstream theorems alpha_over_sigma_pos and r_min_pos inside the same module. It supplies the positivity step required to bridge the Recognition Science strong-coupling value to nuclear binding energies while remaining inside the forcing chain that fixes alpha_s via geometric constraints.
scope and limits
- Does not establish the numerical value of alpha_strong beyond the fixed rational 2/17.
- Does not incorporate the running of the coupling with momentum scale.
- Does not address non-perturbative confinement or higher-order QCD corrections.
Lean usage
exact div_pos alpha_strong_pos stringTension_posformal statement (Lean)
38theorem alpha_strong_pos : 0 < alpha_strong := by
proof body
Term-mode proof.
39 unfold alpha_strong alpha_s_geom; norm_num
40
41/-- String tension is positive. -/