alpha_strong
plain-language theorem explainer
Strong coupling constant α_s is defined as the real embedding of the rational 2/17 obtained from wallpaper group geometry. Nuclear modelers deriving Cornell potentials or SEMF coefficients from QCD inputs would cite this value when scaling between strong-force parameters and nuclear radii. The definition performs a direct cast from the upstream geometric fraction into real arithmetic.
Claim. The strong coupling constant is given by $α_s = 2/17$.
background
Recognition Science obtains the strong coupling from wallpaper fractions, with the upstream definition supplying the exact rational 2/17. The module bridges this QCD-level value together with string tension σ = φ^{-5} to the nuclear semi-empirical mass formula coefficients. All results in the module are machine-verified with zero sorry or axiom.
proof idea
One-line definition that casts the rational alpha_s_geom into real numbers.
why it matters
This supplies the fixed α_s value used by eight downstream declarations, including positivity of α_s/σ, the Cornell potential at r₀ ≈ 1.2 fm, and strong-versus-electromagnetic comparisons. It occupies the QCD-to-nuclear bridge step where the geometric input α_s = 2/17 enters nuclear-scale calculations.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.