alpha_s_err
plain-language theorem explainer
The definition supplies the PDG uncertainty 0.0009 on the strong coupling at the Z scale. Recognition Science derivations of alpha_s from wallpaper symmetry groups cite it to certify that the exact prediction 2/17 lies inside the measured interval. The declaration is a direct numeric assignment with no computation or lemmas.
Claim. $alpha_s^{err} := 0.0009$
background
In the StrongForce module the strong coupling is obtained from the reciprocal of half the wallpaper group count, yielding the exact prediction $alpha_s = 2/17$. The module imports the constants package and the alpha derivation to place this value in the Recognition Science ledger. The experimental anchor is the PDG 2022 measurement $alpha_s(M_Z) = 0.1179 pm 0.0009$, which the present definition records as the uncertainty bound.
proof idea
The declaration is a direct numeric assignment of the real number 0.0009. No lemmas or tactics are applied; the value is taken from the PDG 2022 compilation as stated in the module documentation.
why it matters
This error bound closes the T15 certificate by supplying the tolerance that makes the wallpaper prediction match experiment. It is referenced by the theorem alpha_s_match, which proves the absolute difference between prediction and measurement is smaller than the declared error, and by the T15Cert structure that packages the geometric origin together with the match. Within the Recognition framework it completes the strong-force step by confirming consistency with observation at the 0.2 sigma level.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.