W_exact
plain-language theorem explainer
The lemma fixes the number of distinct 2D wallpaper groups at exactly 17 when embedded in the reals. Lepton mass derivations in the Recognition framework cite it to anchor the muon-to-tau step function. The proof is a one-line wrapper that unfolds the constant definition and normalizes the integer.
Claim. The number of distinct two-dimensional wallpaper groups equals exactly 17.
background
Module T10 Necessity derives the lepton ladder from T9 electron mass plus geometric inputs. Wallpaper groups denotes the 17 distinct 2D symmetry classes, a crystallographic constant established by Fedorov in 1891. The definition appears in AlphaDerivation as wallpaper_groups : ℕ := 17 and is cast to ℝ for arithmetic with cube faces, passive edges, and alpha.
proof idea
One-line wrapper that applies the definition of wallpaper_groups then normalizes the numeric literal 17.
why it matters
Supplies the exact W = 17 required by lepton_ladder_forced_from_T9, which writes the muon-tau step as 6 - (2*17 + D)/2 * alpha. It closes the crystallographic input for the T10 forcing chain that links cube geometry and the eight-tick octave to observed lepton masses. No open scaffolding remains.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.