strong_vs_em
plain-language theorem explainer
The theorem establishes that the Recognition Science strong coupling exceeds the electromagnetic fine-structure constant. Nuclear modelers deriving binding energies from QCD inputs would cite this inequality to confirm force hierarchy before applying the semi-empirical mass formula. The proof reduces to unfolding the two definitions and invoking norm_num on the resulting numerical comparison.
Claim. $1/137 < 2/17$ where $2/17$ is the strong coupling constant obtained by casting the wallpaper fraction to reals.
background
The QCD-to-Nuclear Bridge module converts the QCD-level description (strong coupling from wallpaper groups, string tension equal to phi to the minus five) into coefficients of the semi-empirical mass formula. The local setting treats alpha_strong as the real cast of the geometric alpha_s. Upstream, alpha_s_geom is defined as the rational 2/17 and labeled the Wallpaper Fraction and Predicted Strong Coupling; alpha_strong simply re-exports that value in reals.
proof idea
The proof is a one-line term-mode wrapper. It unfolds alpha_strong and alpha_s_geom, then applies norm_num to discharge the numerical inequality.
why it matters
The result supplies the force-strength ordering required by the module's bridge to the semi-empirical mass formula. It sits inside the Recognition Science alpha band (137.030 to 137.039) and inherits the geometric origin of couplings from the wallpaper construction. No downstream theorems are recorded yet, so the inequality functions as a foundational check rather than an input to further derivations.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.