wallpaper_group_count
plain-language theorem explainer
Exactly seventeen planar crystallographic (wallpaper) groups exist, fixed by counting a finite enumeration of the classical types. Anyone anchoring the Recognition Science endogenous W=17 bridge to cube-face structure cites this as the external classical count. The proof is a one-line native decision on the derived Fintype instance for that enumeration.
Claim. The number of wallpaper groups is exactly $17$: if $\mathcal{W}$ denotes the finite set of classical planar crystallographic groups (oblique, rectangular, square, and hexagonal types), then $|\mathcal{W}| = 17$.
background
Wallpaper groups are the discrete groups of isometries of the Euclidean plane that contain two independent translations (planar crystallographic groups). Classically there are seventeen conjugacy classes, labeled p1, p2, pm, pg, cm, pmm, pmg, pgg, cmm, p4, p4m, p4g, p3, p3m1, p31m, p6, p6m, after Fedorov (1891).
This module builds an endogenous bridge from the 3-cube: six square faces, each with dihedral stabilizer $D_4$, plus a triangular decomposition that accounts for the five hexagonal groups, aiming at $W = E_{\mathrm{passive}} + F = 11 + 6 = 17$ when spatial dimension is three.
Upstream, the inductive type enumerates those seventeen labels and derives Fintype and DecidableEq. The present theorem simply records that the derived finite cardinality equals seventeen, matching the classical external count the bridge is meant to recover.
proof idea
One-line tactic proof. The inductive enumeration of wallpaper groups carries a derived Fintype instance, so Fintype.card is a closed natural-number term. native_decide evaluates that cardinality in the kernel and checks equality with 17. No lemmas beyond the derived instances are invoked.
why it matters
Recognition Science wants $W=17$ as an endogenous consequence of $D=3$ cube geometry (module claim: $W_{\mathrm{endogenous}}(D) :=$ passive field edges plus cube faces equals 17 iff $D=3$), tying into the forcing chain landmark T8 that spatial dimension is three. This theorem supplies the classical external anchor: the enumerated type really has seventeen inhabitants, so later equalities such as the structural split into edge-generated and face-generated groups can target the same integer.
It does not itself prove endogeneity or the cube decomposition; those live in sibling results (W_eq_17, edge/face dominant counts, W_decomposition). With no downstream users yet recorded, it is a verification pin rather than a lemma in a long chain. It closes the bookkeeping gap between the named inductive constructors and the integer 17 used throughout the wallpaper bridge.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.