coupling_coeff_decomposition
plain-language theorem explainer
The declaration shows that the wallpaper-coupling coefficient evaluates to 37. Researchers deriving sub-leading corrections to lepton masses would reference this to fix the prefactor in the muon-to-tau term as (2W + 3)α/2 with the numerical value 37. The proof reduces to a direct numerical check on the definition involving 17 wallpaper groups and three spatial dimensions.
Claim. The wallpaper coupling coefficient, defined as twice the wallpaper group count plus the spatial dimension, equals 37.
background
The module addresses geometric forcing for sub-leading corrections in lepton generations beyond the integer cube counts. For the muon-to-tau transition the correction takes the form F minus (2W+3)α/2, where the coefficient combines the wallpaper count W=17 with dimension D=3. The upstream definition states that the wallpaper-coupling coefficient is twice the wallpaper groups plus D. This constrains the form of perturbative refinements to the integer cube counts E_pass=11 and F=6, with the spherical term normalized by 1/(4π) in D=3.
proof idea
The proof is a one-line term proof that applies native_decide to verify the arithmetic equality 2*17 + 3 = 37 on the natural numbers.
why it matters
This result fixes the numerical coefficient 37 for the μ→τ coupling term in the lepton mass corrections. It draws on the dimensional requirement D=3 from the forcing chain and the wallpaper count from the cube structure. The module notes that this supports the corrections being O(1) or smaller, consistent with perturbative refinements of integer structure. It touches the open question of full uniqueness of the correction form.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.