alpha_s_pred
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 in Recognition Science
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.
scope and limits
- Does not derive the wallpaper group count W=17 from more primitive axioms.
- Does not include renormalization-group running of the coupling.
- Does not compute higher-order QCD corrections or lattice effects.
- Does not address unification at GUT scales beyond the M_Z value.
Lean usage
theorem check : alpha_s_pred = (2 : ℝ)/17 := by simp [alpha_s_pred]formal statement (Lean)
47noncomputable def alpha_s_pred : ℝ := alpha_s_geom
proof body
Definition body.
48
49/-! ## Geometric Derivation -/
50
51/-- The prediction derives from wallpaper group count. -/