SymmetryType
plain-language theorem explainer
Two-valued tag that marks each wallpaper group as edge-dominant or face-dominant. Downstream classification maps the 17 groups onto this tag so the count splits as 11 + 6. Pure data definition with decidable equality; no proof content.
Claim. An inductive type with two constructors: $\mathrm{Edge}$ and $\mathrm{Face}$. It labels whether a planar symmetry group is generated primarily by 1D edge-type operations or by 2D face-type rotational symmetries. Equality on the type is decidable.
background
The module builds an endogenous bridge from the 3-cube to the classical count $W=17$ of wallpaper groups (Fedorov 1891). The structural claim is
$$W = (\text{edge-generated}) + (\text{face-generated}) = E_{\mathrm{passive}} + F = 11 + 6 = 17.$$
Edge-generated groups arise from 1D symmetry directions along the 11 passive field edges (translations, reflections, glides). Face-generated groups arise from the 2D rotational symmetries of the 6 cube faces, whose stabilizers are dihedral $D_4$ and, via triangular decomposition, the hexagonal families.
Upstream, Edge in MultiDistinctionGeometry is the four-sided orientation type of a square ($B,T,L,R$). The present type is coarser: it only records which of the two generation modes dominates a full wallpaper group, not which geometric edge is involved.
proof idea
No proof. The declaration is a two-constructor inductive type with derived DecidableEq and Repr. It supplies the codomain for the classification map that assigns each of the 17 named wallpaper groups to either edge-dominant or face-dominant.
why it matters
This tag is the codomain of dominantType, which classifies every wallpaper group by generation mode (e.g. pure translation and edge-midpoint 180° rotations as edge-type; square and hexagonal rotational families as face-type). That classification underwrites the sibling equalities edge_dominant_eq_Ep and face_dominant_eq_F, and thereby the decomposition $W = E_{\mathrm{passive}} + F = 17$.
In the Recognition chain the count is forced only at $D=3$ (T8), matching the cube-intrinsic formula $W_{\mathrm{endogenous}}(D) := E_{\mathrm{passive}}(D) + F(D)$. The type itself is scaffolding for that bridge: without a clean Edge/Face split the endogenous 11+6 accounting cannot be stated inside Lean.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.