alpha_s_exp
plain-language theorem explainer
This definition supplies the PDG 2022 experimental value 0.1179 for the strong coupling constant alpha_s at the Z mass. Recognition Science derivations cite it when checking the geometric prediction 2/17 against measured data in the T15 verification. The entry is a bare numeric constant assignment with no computation or hypotheses.
Claim. The experimental value of the strong coupling constant is defined by $alpha_s^{exp} := 0.1179$.
background
The StrongForce module formalizes T15, the derivation of the strong coupling from planar symmetries of the ledger. While the fine-structure constant alpha follows from full edge geometry, alpha_s is the reciprocal of half the wallpaper-group count W=17, so the geometric prediction is 2/17. The module imports Constants and AlphaDerivation; the experimental anchor supplied here is the PDG 2022 measurement 0.1179 with stated uncertainty 0.0009.
proof idea
This is a direct definition that binds the real number 0.1179 to alpha_s_exp. No lemmas, tactics, or reductions are applied.
why it matters
The value is required by the alpha_s_match theorem, which shows the geometric prediction lies inside the experimental error band, and by the T15Cert structure that records both the wallpaper-group origin and the PDG match. It completes the verification step for the strong force in the Recognition framework, where alpha_s = 2/W closes the symmetry-count argument begun in the alpha derivation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.