dominantType
plain-language theorem explainer
Assigns each of the 17 wallpaper groups a dominant symmetry type: Edge (1D generators) or Face (2D face structure). Eleven groups are edge-dominant and six face-dominant. Downstream counts use this map to prove the structural split 11 + 6 = 17 = W. The definition is an exhaustive case split on the group enumeration.
Claim. A function from the set of 17 wallpaper groups to $\{\mathrm{Edge},\mathrm{Face}\}$ that labels each group by its dominant generator type: pure translations, 180° rotations, reflections, and glides (and edge-mediated 90° cases) as Edge; full square $D_4$ and all triangular/hexagonal groups as Face.
background
The module bridges Fedorov's classical count of 17 planar symmetry groups to the internal geometry of the 3-cube. Spatial dimension is fixed at $D=3$ (T8/T9). The cube has $F=6$ square faces; each face stabilizer is the dihedral group $D_4$. The endogenous identity is $W_{\mathrm{endogenous}}(D)=E_{\mathrm{passive}}(D)+F(D)$, equal to 17 precisely when $D=3$.
Here the structural claim is sharpened: $W$ splits as edge-generated plus face-generated groups, matching $E_{\mathrm{passive}}+F=11+6$. Edge type means symmetries defined by 1D elements (translations, reflections, glides along lattice directions, including 90° rotations treated as edge-mediated at vertices). Face type means symmetries that require genuine 2D face structure: full square $D_4$, and the five hexagonal groups arising from triangular decomposition of cube faces (each square splits into two triangles; six faces yield twelve triangular facets).
WallpaperGroup enumerates the classical 17 labels (oblique, rectangular, square, hexagonal). SymmetryType is the two-point codomain Edge | Face.
proof idea
Pure definition by exhaustive pattern match on the inductive wallpaper enumeration. No lemmas or tactics: each constructor is assigned Edge or Face by the structural reading above (comments in the body record the geometric rationale). Downstream cardinality filters simply count preimages under this map.
why it matters
This classification is the hinge for the module's structural decomposition $W=(\text{edge-generated})+(\text{face-generated})=E_{\mathrm{passive}}+F$. It feeds edge_dominant_count and face_dominant_count, and thereby the native-decide theorem total_matches_W asserting $11+6=17=W$.
In the Recognition framework this tightens endogeneity of the wallpaper count: the classical 17 is no longer an external Fedorov input but a split aligned with cube edges and faces at $D=3$ (forcing chain T8). The face branch also ties hexagonal groups to triangular face decomposition, linking cube geometry to dual-polyhedral (icosahedral) facet counts. Parent goal remains full endogenous derivation of $W=17$ from cube-intrinsic data alone.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.