strongCouplingRS
plain-language theorem explainer
The definition assigns the rational value 2/17 to the Recognition Science prediction for the strong coupling constant at the Z scale. QCD phenomenologists comparing RS wallpaper-fraction results to PDG data would cite this constant when verifying the five-parameter count against measured α_s(M_Z). The assignment is a direct constant block with no computation or lemmas required.
Claim. The Recognition Science prediction for the strong coupling constant at the Z-boson mass scale is defined as $2/17$.
background
The Strong Nuclear Force from RS module derives α_s(M_Z) from a wallpaper-fraction argument that equates five QCD parameters (α_s together with the u/d/s, c/b and top mass sets) to the configuration dimension D. The module comment states that α_s(M_Z) ≈ 0.1176 with the RS value 2/17 = 0.1176..., obtained inside the broader Recognition Science framework that starts from the J-cost functional equation and the phi-ladder fixed point. No upstream results are referenced for this constant.
proof idea
Direct definition that sets the constant to the rational 2/17. No lemmas are applied and no tactics are used; the value is supplied verbatim from the wallpaper-fraction derivation.
why it matters
The constant is used by StrongForceCert, alphaSRS_near_PDG, strongCoupling_approx and strongCouplingRS_eq to certify that 2/17 lies inside the PDG band of width 0.001. It supplies the RS value for the strong force inside the T0-T8 forcing chain where D = 3 fixes the parameter count at five and the eight-tick octave constrains the discrete spectrum. The open question left in the module is whether the wallpaper-fraction counting argument can be turned into a formal theorem.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.