edge_dominant_count
plain-language theorem explainer
Defines the number of wallpaper groups whose dominant symmetry is edge-type (1D translations, reflections, glides). Anyone citing the endogenous W = E_passive + F split uses this count. The body is a pure Finset filter-and-card over the enumerated 17 groups via the dominant-type classifier.
Claim. Let $\mathcal{W}$ be the set of 17 wallpaper groups. Write $\mathrm{dom}(g)$ for the dominant symmetry type of $g$ (edge versus face). Then the edge-dominant count is $\#\{ g \in \mathcal{W} : \mathrm{dom}(g) = \mathrm{Edge} \}$.
background
The module bridges the classical Fedorov count $W = 17$ of planar symmetry groups to cube-intrinsic structure in $D = 3$. Wallpaper groups are enumerated as an inductive type covering the oblique, rectangular, square, and hexagonal families. Each group is labeled by a dominant symmetry type: edge-dominant means the defining symmetries are essentially 1D (translations, edge-midpoint $180^\circ$ rotations, reflections or glides along edge directions); face-dominant means 2D rotational content of a square face.
The intended structural split is $W = $ (edge-generated) $+$ (face-generated) $= E_{\mathrm{passive}} + F = 11 + 6 = 17$, matching the cube-endogenous identity $W_{\mathrm{endogenous}}(D) := $ passive field edges $+ $ cube faces, which equals 17 iff $D = 3$.
Upstream, dominantType assigns each enumerated group to Edge or Face; the Edge constructor of the multi-distinction geometry (oriented square sides B/T/L/R) supplies the 1D language behind that label.
proof idea
Not a proof: a definition. Take the finite universe of all wallpaper groups, keep those with dominant type equal to Edge, and return the cardinality of that filter. Decidable equality on the symmetry-type enum makes the filter computable; later theorems discharge the numeric value by native_decide.
why it matters
This count is the left summand in the structural decomposition $W = $ edge-dominant $+$ face-dominant. Downstream, edge_dominant_eq_Ep asserts the count equals 11, and total_matches_W asserts $11 + 6 = 17 = W$. Together they strengthen the endogenous bridge from cube faces and passive edges to the classical wallpaper census, aligning with the $D = 3$ forcing landmark (T8) and the cube-face story ($F = 6$, $D_4$ stabilizers, triangular facets feeding the five hexagonal groups).
It does not invent new physics constants; it packages the combinatorial half of the $E_{\mathrm{passive}} + F$ identity so the verification layer can cite a single natural-number definition rather than an ad-hoc list.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.