WallpaperGroup
plain-language theorem explainer
Enumerates the classical 17 wallpaper groups (p1 through p6m), partitioned by lattice class: oblique, rectangular, square, hexagonal. Downstream counts and the edge/face dominance split are defined over this finite type. The declaration is a pure inductive with DecidableEq, Repr, and Fintype instances; cardinality 17 is discharged by native_decide.
Claim. The type of wallpaper groups is the finite enumeration $\{p1, p2, pm, pg, cm, pmm, pmg, pgg, cmm, p4, p4m, p4g, p3, p3m1, p31m, p6, p6m\}$, i.e. the 17 distinct discrete isometry groups of the Euclidean plane that preserve a lattice (Fedorov 1891).
background
Wallpaper groups are the crystallographic point-plus-lattice symmetries of the plane: combinations of translations, rotations, reflections, and glides compatible with a 2D lattice. Classically there are exactly 17, proved by Fedorov (1891).
This module builds an endogenous bridge from the 3-cube to that count. The cube has $F=6$ square faces; each face stabilizer is the dihedral group $D_4$. $D_4$ is compatible with the oblique, rectangular, and square lattice classes (2+7+3 groups). The five hexagonal groups are tied to a triangular decomposition of the cube faces (6 faces $\to$ 12 triangular facets).
The structural claim is $W = E_{\mathrm{passive}} + F = 11 + 6 = 17$, with 11 edge-generated and 6 face-generated groups. This inductive supplies the named carriers for that split.
proof idea
No proof body: pure inductive definition. Constructors are the standard IUCr labels, grouped by lattice class in comments (oblique 2, rectangular 7, square 3, hexagonal 5). Derives DecidableEq, Repr, and Fintype so that Finset.univ and native_decide can count and filter the type in sibling definitions.
why it matters
This is the carrier type for the wallpaper classification bridge. Parent uses include wallpaper_group_count (Fintype.card = 17 by native_decide), dominantType (maps each group to Edge or Face symmetry), and the two filtered counts edge_dominant_count and face_dominant_count that realize the decomposition $W = 11 + 6$.
In the Recognition framework the target identity is $W_{\mathrm{endogenous}}(D) := E_{\mathrm{passive}}(D) + F(D) = 17$ iff $D=3$, linking the classical Fedorov count to the forced spatial dimension (T8). The enumeration makes the edge-versus-face structural split checkable inside Lean rather than a bare numeral 17.
It does not yet prove that the classical groups arise from cube face stabilizers; it only names them so the bridge lemmas can classify and count.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.