coupling_half
The wallpaper coupling coefficient equals 37 when formed as twice the wallpaper group count plus three spatial dimensions. Dividing by two therefore yields exactly 37/2. This arithmetic fact supplies the prefactor in the geometric correction term for the muon-to-tau mass step. The proof is a direct numerical check performed by the native decision procedure on the rational cast of the coefficient.
claimLet $W$ be the wallpaper group count and $D=3$ the spatial dimension. Define the wallpaper coupling coefficient by $c=2W+D$. Then $c/2=37/2$.
background
The Lepton Sub-Leading Forcing module treats corrections to lepton generation steps beyond the integer cube counts E_pass=11 and F=6. The wallpaper coupling coefficient is defined as twice the wallpaper group count plus the spatial dimension D, producing the integer 37. This coefficient appears in the correction (2W+3)α/2 for the μ→τ transition, while the spherical term 1/(4π) supplies the unique solid-angle normalization in three dimensions.
proof idea
The proof is a one-line term that applies native_decide after casting the natural-number wallpaper coupling coefficient to a rational. The tactic evaluates the division by 2 and confirms equality to 37/2 using the definition c=2*wallpaper_groups+D.
why it matters in Recognition Science
The result fixes the numerical value of the wallpaper prefactor that constrains sub-leading corrections in the lepton mass formula. It closes the arithmetic verification step required by the module's geometric-forcing argument, consistent with D=3 and the cube structure in the Recognition Science chain. No downstream theorems are listed, but the identity supports bounds on O(1) perturbative refinements of the phi-ladder mass formula.
scope and limits
- Does not prove that 37 is the only possible coefficient arising from cube geometry.
- Does not derive the wallpaper group count W from first principles.
- Does not connect the coefficient to measured lepton mass ratios.
- Does not bound higher-order terms beyond the stated O(1) scale.
formal statement (Lean)
85theorem coupling_half : (wallpaper_coupling_coeff : ℚ) / 2 = 37 / 2 := by native_decide
proof body
Term-mode proof.
86
87/-! ## Correction Bounds -/
88
89/-- The spherical correction 1/(4π) is between 0.079 and 0.080. -/