alphaStrong
plain-language theorem explainer
Defines the RS strong coupling as the exact rational α_s = 2/17 (wallpaper-group fraction). Cited wherever Item 8 residual families need a frozen quark-sector coupling κ. The body is a one-line constant assignment; agreement with PDG α_s(M_Z) is claimed externally at ~0.3σ, not proved here.
Claim. The Recognition Science strong coupling is the constant $\alpha_s := 2/17$.
background
Item 8 of the verification stack concerns sub-leading mass residuals on the φ-ladder: after the integer rung step is stripped, a signed residual measures the leftover correction in rung units. The module builds a sign-split ratio family whose sector couplings κ enter those residual predictions.
In that family the quark sectors are assigned a common coupling identified with the strong fine-structure constant. The RS claim is that this coupling is not a free fit parameter but the exact wallpaper-group fraction 2/17 ≈ 0.11765, to be compared with PDG α_s(M_Z) = 0.1179 ± 0.0009.
Related constants in the broader stack (α^{-1} residual bands, φ-ladder rung types, finite-N channel corrections) supply the surrounding numerical language; this definition only freezes the strong-sector κ used by the Item 8 targets.
proof idea
Pure definition: the real constant is assigned the literal value 2/17. No lemmas, tactics, or reduction steps.
why it matters
Freezes κ = α_s for every specialized Item 8 closure in this module. Downstream, item8Specialized asserts both quark residual pairs fit the sign-split family at this coupling; allSectorTest and the refined variants reuse it as the up/down quark signature coupling while testing lepton out-of-sample residuals. Lepton-anchored predictions and the two down-anchor cPos expressions likewise insert α_s into the transported residual formulas.
Within the RS primer this is the strong-sector counterpart of the electromagnetic α band: a pure rational fixed by discrete structure (here a wallpaper-group fraction) rather than a running fit. Closing Item 8 with this value would make the all-sector residual family falsifiable against PDG masses without a free κ.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.