alpha_s_match
plain-language theorem explainer
The theorem confirms that the strong coupling predicted as 2/17 lies within 0.000253 of the measured central value 0.1179 and satisfies the experimental error bound of 0.0009. Gauge unification researchers and Recognition Science modelers cite it to validate the wallpaper symmetry derivation of α_s(M_Z). The proof reduces the inequality to a direct numerical check by unfolding the four definitions and normalizing the resulting real arithmetic.
Claim. $|2/17 - 0.1179| < 0.0009$, where $2/17$ is the predicted strong coupling from wallpaper group count, 0.1179 is the experimental central value, and 0.0009 is the reported uncertainty.
background
The StrongForce module treats the strong coupling as arising from planar symmetries of the ledger, with α_s = 2/W for wallpaper group count W = 17. The geometric prediction is encoded as the rational alpha_s_geom = 2/17, lifted to the real alpha_s_pred; the experimental inputs are the constant alpha_s_exp = 0.1179 and error alpha_s_err = 0.0009, matching PDG 2022 data at the Z scale. The local setting distinguishes this from the electromagnetic α derived from full edge geometry (4π · 11).
proof idea
The term proof applies simp to unfold alpha_s_pred, alpha_s_geom, alpha_s_exp, and alpha_s_err, then invokes norm_num to evaluate the absolute difference and confirm it lies strictly below the error bound.
why it matters
This supplies the numerical verification required by t15_verified to certify the T15 geometric origin and is invoked directly by alpha_s_within_pdg_bounds to place α_s inside PDG error bars. The module document states that the strong coupling is now formally proven from the wallpaper fraction rather than axiomatized, anchoring the geometric interpretation inside the unified forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.