alpha_s_pred
plain-language theorem explainer
The definition sets the predicted strong coupling α_s^pred equal to the geometric wallpaper fraction 2/17. Gauge unification researchers cite it when verifying the T15 prediction against PDG measurements of α_s(M_Z). The declaration is a direct abbreviation of the rational constant alpha_s_geom expressed over the reals.
Claim. $α_s^{pred} := 2/17$
background
The StrongForce module derives the strong coupling from planar symmetries of the ledger. The module hypothesis states that the strong force couples to pairs of symmetries, so α_s equals 2 over the wallpaper group count W=17, yielding ≈0.11765 and matching the PDG 2022 value 0.1179 ± 0.0009 within 0.2σ. Upstream, the from theorem reduces seven axioms to four structural conditions plus definitional facts, while alpha_s_geom fixes the exact rational 2/17.
proof idea
One-line abbreviation that aliases alpha_s_geom (the wallpaper fraction 2/17) to real type for downstream arithmetic.
why it matters
Supplies the core value for T15Cert, alpha_s_match, and alpha_s_pred_eq_two_over_W. It fills the C-014.2 proposition on strong coupling derived from wallpaper groups and feeds alpha_s_coupling_derived plus alpha_s_within_pdg_bounds in GaugeCouplingsComplete. The result anchors the symmetry-based derivation of gauge couplings within the Recognition framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.