edge_dominant_eq_Ep

This module bridges the classical count of seventeen wallpaper groups (Fedorov 1891) to the internal face structure of the 3-cube. The cube has six square faces; each face stabilizer is the dihedral group $D_4$. The module partitions the seventeen groups into edge-generated and face-generated classes so that $W = E_{\mathrm{passive}} + F = 11 + 6$.

edge_dominant_count is the cardinality of the finite set of WallpaperGroup values whose dominantType equals the edge tag. Edge-dominant groups are those whose generating symmetries are one-dimensional (translations and reflections along the eleven passive field edges of the cube). The companion count for face-dominant groups is six.

The local claim is purely enumerative: once the seventeen groups and their dominant-type tags are fixed as a decidable finite type, the edge slice has size eleven.

One-line computational proof: native_decide evaluates the Finset filter (Finset.univ.filter (fun g => dominantType g == .Edge)).card over the finite enumerated type WallpaperGroup and checks equality with the numeral 11. No algebraic lemmas are invoked; the result is a kernel-checked decision of a closed finite computation.

The equality pins the first summand in the structural decomposition $W = $(edge-generated$) + $(face-generated$) = 11 + 6 = 17$ advertised in the module. That decomposition strengthens the endogenous bridge from cube geometry to the classical wallpaper count, complementing the earlier identity $W_{\mathrm{endogenous}}(D) = E_{\mathrm{passive}}(D) + F(D) = 17$ if and only if $D = 3$ (forcing-chain landmark T8). With no downstream dependents yet, the theorem is a leaf certificate that the edge half of the 11+6 split is numerically exact once the dominant-type tagging is fixed.