edge_generated_groups
plain-language theorem explainer
Names the count of wallpaper groups generated by one-dimensional (edge-type) symmetries as the passive field-edge count of the D-cube. For the forced spatial dimension D = 3 this is 11, covering translations, edge-perpendicular reflections, and glides. Cited by the structural split W = edge-generated + face-generated. The definition is a one-line alias of passive_field_edges at D.
Claim. Define the number of edge-generated wallpaper groups to be the number of passive field edges of the $D$-cube, $E_{\mathrm{passive}}(D) := e(D) - e_{\mathrm{active}}$, where $D = 3$ is the forced spatial dimension. Numerically this equals $11$.
background
The module builds an endogenous bridge from the 3-cube to the classical count of 17 wallpaper groups (Fedorov 1891). The structural claim is $W = E_{\mathrm{passive}} + F = 11 + 6 = 17$: eleven groups arise from 1D edge-type generators and six from 2D face-type generators.
Spatial dimension is fixed at $D = 3$ by the forcing chain (T8/T9). The hypercube has $e(D) = D \cdot 2^{D-1}$ edges; one active edge is reserved per tick, so the passive (field) edges are $e(D) - 1$. For $D = 3$ this is $12 - 1 = 11$. Those eleven directions supply translations along edges, reflections across edge-perpendicular planes, and glide reflections.
The companion count is the six cube faces, each carrying a $D_4$ stabilizer compatible with the rectangular and square lattice classes; hexagonal groups are tied to triangular face decompositions elsewhere in the bridge.
proof idea
Pure definitional abbreviation: the value is exactly passive_field_edges D with D := 3 from the alpha-derivation constants. No tactics or lemmas; evaluation is by unfolding the cube-edge formula and subtracting the single active edge per tick.
why it matters
Supplies the first summand in the structural decomposition used by W_decomposition and W_eq_17, which prove edge-generated + face-generated equals the wallpaper count and equals 17 by native decision. That split is the module's strengthening of the earlier endogenous identity $W_{\mathrm{endogenous}}(D) = E_{\mathrm{passive}}(D) + F(D)$, true iff $D = 3$.
In the Recognition framework this ties the classical planar classification to cube combinatorics forced by T8 ($D = 3$) and the passive-edge dressing of interactions in the alpha derivation. It does not yet classify each of the 17 groups by name; it only anchors the 11-vs-6 generator split that makes $W = 17$ cube-intrinsic.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.