W_exact
plain-language theorem explainer
The lemma establishes that the number of distinct two-dimensional wallpaper groups equals exactly 17. Researchers deriving forced lepton mass ladders from T9 in Recognition Science cite this to anchor the W term in the step_mu_tau expression. The proof is a one-line wrapper that unfolds the constant definition and evaluates it numerically.
Claim. Let $W$ denote the number of distinct two-dimensional wallpaper groups. Then $W = 17$.
background
The T10 module proves the lepton ladder is forced from the electron mass (T9) together with cube-derived quantities: passive edges $E_p = 11$, faces $F = 6$, wallpaper groups $W$, the fine-structure constant from T6, and spherical geometry via pi. The wallpaper_groups constant enters the denominator of the curvature fraction that determines the mu-to-tau step. Upstream, wallpaper_groups is the standard crystallographic count of 17 groups, established by Fedorov in 1891 and imported from AlphaDerivation and AlphaHigherOrder.
proof idea
This is a one-line wrapper that applies simp only [wallpaper_groups] to unfold the definition, followed by norm_num to reduce the constant 17 to equality in the reals.
why it matters
The result supplies the exact W value required by the parent theorems lepton_ladder_forced_from_T9 and lepton_ladder_forced_from_T9_v2, which derive the forced steps step_e_mu and step_mu_tau and the resulting muon and tau mass predictions. It closes the crystallography input into the T10 necessity chain, consistent with the eight-tick octave and D = 3 spatial dimensions of the broader framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.