alpha_over_sigma_gt_one
plain-language theorem explainer
The theorem establishes that the strong coupling constant exceeds the string tension in Recognition Science units. Nuclear physicists deriving semi-empirical mass formula coefficients from QCD parameters would cite this inequality. The proof substitutes the explicit value 2/17 for alpha_strong and applies the known bounds on string tension to verify the inequality via cross-multiplication and division properties.
Claim. $1 < 2/17 / σ$ where $σ = φ^{-5}$ is the string tension in RS units.
background
The QCDToNuclearBridge module connects the strong force at the QCD level, with coupling α_s = 2/17 from wallpaper groups and string tension σ = φ^{-5}, to the nuclear semi-empirical mass formula coefficients. Key definitions are alpha_strong as the real number obtained from alpha_s_geom and stringTension as Constants.phi raised to the power -5. Upstream results supply the geometric origin of the strong coupling and the positivity plus upper bound on string tension.
proof idea
The tactic proof unfolds alpha_strong to obtain equality with 2/17. It invokes stringTension_bounds and stringTension_pos to establish positivity and the upper bound stringTension < 2/17. A calc block rewrites 1 as stringTension/stringTension and applies div_lt_div_of_pos_right together with nlinarith to reach the target inequality.
why it matters
This inequality supports the bridge from QCD parameters to nuclear binding energies within the Recognition Science framework. It relies on the fixed values α_s = 2/17 and σ = φ^{-5} derived from the phi-ladder. The result contributes to the module-wide verification that all theorems are machine-checked with zero sorry.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.