face_dominant_count
plain-language theorem explainer
Counts how many of the 17 wallpaper groups are face-dominant: those whose dominant symmetry is 2D (face) rather than 1D (edge). Anyone citing the endogenous W = E_passive + F decomposition uses this integer. It is a pure cardinality definition: filter the finite WallpaperGroup enumeration by dominant type Face and take the card.
Claim. Let $\mathrm{WG}$ be the finite set of the 17 wallpaper groups, and let $\tau(g)\in\{\mathrm{Edge},\mathrm{Face}\}$ be the dominant symmetry type of $g$. Define $N_{\mathrm{face}}:=\#\{g\in\mathrm{WG}:\tau(g)=\mathrm{Face}\}$.
background
The module bridges the classical count $W=17$ of planar wallpaper groups (Fedorov 1891) to the internal face structure of the 3-cube, aiming at an endogenous derivation of $W$. The cube has $F=6$ square faces; each face stabilizer is the dihedral group $D_4$. The structural claim is $W=(\text{edge-generated})+(\text{face-generated})=E_{\mathrm{passive}}+F=11+6=17$.
WallpaperGroup is an inductive enumeration of the 17 classical groups (oblique, rectangular, square, hexagonal). dominantType assigns each group a SymmetryType: Edge when the symmetry is essentially 1D (translations, glides, reflections along edge directions), Face when 2D rotational content of a face dominates. Face-dominant groups are the ones counted here.
proof idea
Definition, not a theorem. On the finite type of all wallpaper groups, form the Finset of those $g$ with dominantType g = Face, then take .card. No lemmas are applied; the value is later discharged by native_decide in the equality theorems.
why it matters
This integer is the face half of the structural decomposition $W=E_{\mathrm{passive}}+F$. Downstream, face_dominant_eq_F proves the count equals 6, and total_matches_W proves edge-dominant count plus this count equals the wallpaper total 17. Together they support the module claim that six face-generated groups arise from the six cube faces (with the remaining eleven edge-generated), tying $W=17$ to $D=3$ cube geometry and the endogenous bridge $W_{\mathrm{endogenous}}(D)=E_{\mathrm{passive}}(D)+F(D)$ forced at $D=3$ (T8).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.