alphaSRS_near_PDG
plain-language theorem explainer
The RS framework predicts the strong coupling α_s(M_Z) exactly as 2/17. QCD model builders would cite this result when validating the wallpaper-fraction derivation against the PDG benchmark. The proof is a one-line term reduction that unfolds the two constant definitions and applies norm_num.
Claim. The absolute difference between the Recognition Science strong coupling constant $2/17$ and the PDG value $0.118$ satisfies $|2/17 - 0.118| < 0.001$.
background
The module Strong Nuclear Force from RS derives α_s(M_Z) via wallpaper fractions, setting the RS value to 2/17 ≈ 0.1176. strongCouplingRS is the rational constant 2/17 while alphaSPDG records the PDG experimental benchmark 0.118. The local setting notes that five QCD parameters (α_s plus quark masses) align with configuration dimension D and that the RS prediction lies close to experiment.
proof idea
The term-mode proof unfolds the definitions of strongCouplingRS and alphaSPDG, then invokes norm_num to discharge the numerical inequality directly.
why it matters
It supplies the near_pdg clause inside the strongForceCert record that certifies the strong force parameters. This closes the experimental comparison for the module's claim α_s(M_Z) = 2/17 from the wallpaper-fraction derivation, supporting RS reproduction of Standard Model constants without extra inputs.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.