alpha_s_pred_eq_two_over_W
plain-language theorem explainer
The equality shows that the predicted strong coupling equals twice the reciprocal of the wallpaper group count. Researchers deriving coupling constants from Recognition Science symmetry counts would reference this when confirming the T15 match to PDG data. The proof reduces directly by unfolding the geometric and predicted expressions for alpha_s and normalizing the resulting arithmetic.
Claim. $alpha_s^{pred} = 2/W$ where $W=17$ is the number of distinct two-dimensional wallpaper groups.
background
The T15 module derives the strong coupling from planar symmetries of the ledger. The wallpaper_groups constant equals 17, the crystallographic count of distinct 2D wallpaper groups established by Fedorov. This count supplies the denominator in the curvature fraction, producing the explicit prediction $alpha_s = 2/W approx 0.11765$ that lies inside the PDG 2022 interval $0.1179 pm 0.0009$ at $0.2sigma$ precision.
proof idea
The proof is a one-line wrapper that applies simp to unfold the definitions of alpha_s_pred, alpha_s_geom, and wallpaper_groups, then invokes norm_num to discharge the resulting numerical equality.
why it matters
This supplies the exact geometric origin required by the T15 certificate t15_verified. It completes the Recognition Science step that sets the strong coupling to twice the reciprocal of the wallpaper-group count, consistent with the module claim that the factor of 2 arises from pairing of symmetries. The result feeds directly into the verified T15Cert structure that packages the equality with the PDG match.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.