face_dominant_eq_F
plain-language theorem explainer
Exactly six of the seventeen wallpaper groups are face-dominant under the cube-face classification. Anyone citing the endogenous W = E_passive + F decomposition (11 + 6 = 17) needs this count. The proof is a one-line native decision on the finite enumeration of WallpaperGroup.
Claim. The number of wallpaper groups whose dominant symmetry type is face-type equals $6$. Equivalently, $\#\{g : \text{wallpaper group} \mid \mathrm{dom}(g)=\mathrm{Face}\}=6$, matching the face count $F=6$ of the $3$-cube.
background
Fedorov’s classical count gives exactly $W=17$ planar crystallographic (wallpaper) groups. This module builds an endogenous bridge from the $3$-cube: six square faces, each with dihedral stabilizer $D_4$, plus passive edge directions, aiming at the structural split $W=E_{\mathrm{passive}}+F=11+6$.
face_dominant_count is the cardinality of the finite filter of WallpaperGroup values whose dominantType equals .Face. The companion edge count is eleven. Upstream abbreviations fix $W:=17$ (wallpaper groups) in the mass and anchor layers; the present lemma only concerns the face half of the split.
The local claim is purely combinatorial: among the seventeen named groups, six are classified face-dominant, matching the geometric face count $F=6$.
proof idea
One-line tactic proof: native_decide evaluates the closed Finset cardinality
(Finset.univ.filter (fun g => dominantType g == .Face)).card
over the finite inductive type WallpaperGroup and checks equality with $6$. No algebraic lemmas are invoked; the decision procedure exhausts the enumerated cases.
why it matters
Closes the face half of the module’s structural identity $W=(\text{edge-generated})+(\text{face-generated})=11+6=17$. The module doc ties the six face-generated groups to $2$D rotational symmetries of the six cube faces (and, via triangular decomposition, to the five hexagonal groups). Together with the sibling edge count, this supports the endogenous bridge $W_{\mathrm{endogenous}}(D)=E_{\mathrm{passive}}(D)+F(D)$ equaling $17$ precisely at $D=3$ (forcing-chain landmark T8). No downstream theorems currently depend on this declaration; it is a verification pin for the classification table itself.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.