Wz_eq
plain-language theorem explainer
The theorem asserts that the integer Wz equals 17. Researchers deriving sector yardsticks for lepton and quark masses in the Recognition Science framework cite this to fix the normalization in the phi-ladder mass formula. The proof is a one-line wrapper that applies simp to unfold Wz and the wallpaper_groups definition.
Claim. $W_z = 17$, where $W_z$ is the integer obtained by casting the number of distinct 2D wallpaper groups.
background
The AnchorDerivation module verifies that sector constants trace to first principles: D=3 from the forcing chain, cube_edges(D)=12, active_edges_per_tick=1, passive_field_edges=11, and wallpaper_groups=17 as the crystallographic constant. Wz is defined locally as the cast of wallpaper_groups to ℤ. Upstream, wallpaper_groups is the standard count of 17 distinct 2D wallpaper groups proven by Fedorov in 1891, used here as the denominator in curvature fractions and face-wallpaper pairs.
proof idea
The proof is a one-line wrapper that applies the simp tactic to the definitions of Wz and wallpaper_groups, which reduces directly to the literal 17.
why it matters
This equality anchors the mass derivation chain by confirming that B_pow and r0 values for leptons, up-quarks, down-quarks, and electroweak sectors follow from the fixed wallpaper_groups count with no free parameters. It supports the first-principles source listed in the module documentation, linking back to T8 (D=3) and cube combinatorics in the Recognition Science framework. No downstream uses are recorded, and the result closes a verification step rather than an open question.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.