W
plain-language theorem explainer
W is the integer constant set to the number of distinct two-dimensional wallpaper groups. Lepton mass derivations in Recognition Science cite this value when assembling the coefficient (2W + 3)/2 for the muon-to-tau step. The definition is a direct one-line alias to the upstream crystallographic constant.
Claim. $W = 17$, the number of distinct 2D wallpaper groups in the Euclidean plane.
background
The module derives the tau generation step from wallpaper symmetry on cube faces coupled to spatial dimension. Wallpaper groups are the 17 distinct 2D symmetry classes classified by Fedorov in 1891. The definition imports this constant from AlphaDerivation.wallpaper_groups and MassTopology.W, where it is fixed at 17 and described as the count of face symmetries.
proof idea
One-line definition that directly aliases wallpaper_groups from the AlphaDerivation module.
why it matters
This supplies the W=17 that produces the coefficient C_τ = W + D/2 = 18.5 in the muon-to-tau formula, matching (2W + 3)/2 exactly. It parametrizes the window length in the canonical recognition cost system of CostAlgebra and traces to the T8 forcing of D=3 together with 2D face mediation in the mass topology.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.