Wz
plain-language theorem explainer
Wz supplies the integer 17 as the count of distinct two-dimensional wallpaper groups for use in sector anchor formulas. Mass modelers cite it when checking alternative r0 expressions for leptons, up quarks, down quarks, and the electroweak sector. The definition is a direct cast of the upstream natural-number constant wallpaper_groups.
Claim. Let $W_z$ denote the integer 17, the number of distinct two-dimensional wallpaper groups.
background
The AnchorDerivation module verifies sector yardsticks derived from cube combinatorics with no free parameters. It traces every constant to D equals 3, cube_edges equal to 12, active_edges_per_tick equal to 1, passive_field_edges equal to 11, and wallpaper_groups equal to 17. Upstream definitions in AlphaDerivation and AlphaHigherOrder introduce wallpaper_groups as the number of distinct 2D wallpaper groups, the base normalization for curvature fractions.
proof idea
One-line wrapper that casts the upstream wallpaper_groups constant from natural numbers to integers.
why it matters
Wz feeds the alternative r0 derivations in r0_alt and the equality proof r0_eq_alt. It anchors the mass ladder to the fixed crystallographic count of 17, consistent with the Recognition Science chain that begins from D equals 3 and cube edge counts. No open questions remain for this constant.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.