wallpaper_coupling_coeff_eq
plain-language theorem explainer
The wallpaper coupling coefficient is fixed at 37 by the arithmetic relation 2W + D, where W counts the wallpaper groups and D is the spatial dimension. Researchers deriving sub-leading corrections to lepton masses would cite this to anchor the prefactor in the muon-to-tau term. The proof evaluates the definition by direct computation.
Claim. $2W + D = 37$, where $W = 17$ is the wallpaper group count and $D = 3$ is the spatial dimension.
background
In the lepton sub-leading corrections module, the integer cube counts E_pass = 11 and F = 6 receive geometric refinements. The muon-to-tau correction takes the form F − (2W + 3)α/2, where the coefficient 2W + D arises from the cube structure with D = 3. The definition wallpaper_coupling_coeff computes exactly this integer 2W + D. Upstream, W is the abbrev for wallpaper_groups = 17 and D is the spatial dimension fixed by the eight-tick octave in the forcing chain.
proof idea
The proof is a one-line wrapper that applies native_decide to evaluate the arithmetic expression in the definition of wallpaper_coupling_coeff.
why it matters
This equality pins the numerical coefficient 37 in the μ→τ sub-leading term, as stated in the module documentation: the factor 37 = 2W + D is forced by the cube structure. It supports the geometric normalization of corrections that remain O(1) or smaller in natural units. The result closes a computational step in the lepton generation forcing without touching open uniqueness questions for the full correction form.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.