wallpaper_coupling_coeff
plain-language theorem explainer
The wallpaper coupling coefficient is the integer 2W + D, with W the number of 2D wallpaper groups and D the spatial dimension. Researchers decomposing the mu to tau lepton mass correction term would cite this coefficient when isolating the geometric factor 37. It is introduced by a direct arithmetic definition that combines the fixed crystallographic count 17 with D equals 3.
Claim. The wallpaper coupling coefficient is defined by the expression $2W + D$, where $W$ is the number of distinct two-dimensional wallpaper groups and $D$ is the spatial dimension.
background
In the Lepton Sub-Leading Corrections module the mu to tau transition correction takes the form $F - (2W+3)alpha/2$. The wallpaper coupling coefficient supplies the integer factor $2W + D$ that appears inside this expression. Upstream, wallpaper_groups is defined as the integer 17, the number of distinct 2D wallpaper groups established by Fedorov in 1891. The dimension $D$ enters from the Recognition Science forcing chain that fixes three spatial dimensions.
proof idea
The declaration is a one-line definition that evaluates twice the value of wallpaper_groups plus D.
why it matters
This coefficient is used by the downstream theorems coupling_coeff_decomposition, coupling_half and wallpaper_coupling_coeff_eq, which verify that the value equals 37 and that division by 2 yields 18.5. It encodes the combination of the wallpaper count 17 with D equals 3 into the sub-leading correction of the lepton mass ladder. The placement links the eight-tick octave structure of the Recognition Science framework to the perturbative alpha term in the mass formula.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.