prediction_eq_two_over_17
plain-language theorem explainer
The preregistered RS point forecast for α_s(M_Z) equals exactly 2/17. Anyone wiring the strong-coupling prediction into a PDG comparison cites this identity. The proof is a one-line simp that unfolds the prediction record and the wallpaper-group constant 17.
Claim. The preregistered point prediction for $\alpha_s(M_Z)$ has numerical value exactly $2/17$.
background
This module holds the preregistered RS forecast for the strong coupling at the Z pole. By design it carries no experimental numbers: only the formula and its algebraic reduction.
The prediction is a PointPrediction whose value is $2$ divided by the number of distinct 2D wallpaper groups. That count is the classical crystallographic constant of Fedorov (1891), fixed here as the natural number 17. The same constant appears in the α-derivation stack as the denominator of the curvature fraction (faces × wallpaper groups).
The companion inverse-fine-structure module preregisters an interval band rather than a point; here the strong-coupling side is a pure rational.
proof idea
Term-mode one-liner. simp unfolds the local prediction record (value field is $2$ over wallpaper_groups) and the definition wallpaper_groups := 17, reducing the goal to the literal equality $2/17 = 2/17$.
why it matters
Locks the RS α_s(M_Z) formula to the concrete rational $2/17$ before any measurement is loaded. Downstream, passes_PDG2022_1sigma reduces its within-sigma check to a numeric inequality against this frozen value, keeping the test stable under PDG updates (only the measurement module changes).
In the broader framework the wallpaper count 17 is the same crystallographic integer that enters the α-derivation denominator; the fine-structure side preregisters the band $(137.030, 137.039)$. This lemma is the algebraic hinge that lets the strong-coupling preregistration stay purely rational and measurement-free.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.