W
plain-language theorem explainer
W denotes the number of distinct two-dimensional wallpaper groups, fixed at 17 by the Fedorov classification. Mass ladder derivations and recognition cost constructions cite this crystallographic constant when normalizing topological fractions from cube geometry in three dimensions. The declaration is a direct one-line alias to the upstream constant without further reduction.
Claim. Let $W$ be the number of distinct two-dimensional wallpaper groups. Then $W = 17$.
background
The Masses.Anchor module assembles parameter-free constants from cube geometry in D=3. Total cube edges equal 12, passive edges equal 11, and W supplies the wallpaper-group count of 17 that appears in sector yardsticks such as lepton r0 = 4W - 6. Upstream results define wallpaper_groups as the standard count of plane symmetry groups, proven by Fedorov in 1891, and reuse it as the denominator of curvature fractions and face-wallpaper pairs.
proof idea
The declaration is a one-line alias to the constant wallpaper_groups imported from AlphaDerivation and AlphaHigherOrder.
why it matters
W supplies the finite window length in the canonical recognition cost system, the structure RecognitionCostSystem n W hW that packages the J-cost, RCL satisfaction, and sigma conservation functional. It anchors downstream theorems on reciprocal symmetry and unit cost at 1, and feeds the mass-topology ledger fractions that close the cube-geometry chain (E_total = 12, D = 3).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.