W_decomposition
plain-language theorem explainer
The classical wallpaper count equals the sum of edge-generated and face-generated planar symmetry groups. Auditors of the endogenous W=17 bridge cite this when matching Fedorov's classification to the 3-cube's passive edges and faces. The proof is a one-line native decision of the concrete natural-number equality.
Claim. The number of edge-generated wallpaper groups plus the number of face-generated wallpaper groups equals the classical wallpaper count: $N_{\mathrm{edge}} + N_{\mathrm{face}} = W$, with $W = 17$.
background
Fedorov (1891) classified the distinct discrete isometry groups of the Euclidean plane compatible with a lattice; there are exactly 17 wallpaper groups. In this module that classical constant is written as a fixed natural wallpaper_groups := 17.
The endogenous bridge ties that count to the 3-cube. The cube has six square faces (each with dihedral stabilizer $D_4$) and eleven passive field edges. The module splits the 17 groups into two structural classes: groups generated from 1D edge symmetries (translations and reflections along passive edges) and groups generated from 2D face symmetries (rotations and reflections of the six faces, plus the five hexagonal groups via triangular face decomposition).
Sibling definitions fix the two summands as concrete naturals (edge class size 11, face class size 6). The parallel result in WEndoForcing states the same split as $W_{\mathrm{endo}}(3) = E_{\mathrm{passive}}(3) + F_{\mathrm{cube}}(3)$.
proof idea
Both summands and the right-hand side are closed natural-number definitions (11, 6, and 17). The proof is the single tactic native_decide, which evaluates the ℕ equality 11 + 6 = 17 by computation. No algebraic lemmas are invoked; the content lives entirely in the definitions of the three constants.
why it matters
This is the structural half of the endogenous wallpaper bridge: $W = N_{\mathrm{edge}} + N_{\mathrm{face}} = E_{\mathrm{passive}} + F = 11 + 6 = 17$. It sits beside the dimensional forcing $W_{\mathrm{endo}}(D) = 17$ iff $D = 3$, which lands on the T8 landmark that spatial dimension is three. Downstream, WEndoForcing.W_decomposition records the same identity in passive-edge and cube-face language (W_endo 3 = passive_field_edges 3 + cube_faces 3). Together they convert an external crystallographic constant into a cube-intrinsic count used in the alpha and curvature normalizations that divide by face-wallpaper pairs.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.