Seventeen wallpaper groups (Pólya–Niggli 1924)

wallpaper_groups_17 — a formalization challenge from the lean-eval benchmark.

Notes

There are exactly 17 wallpaper groups, the discrete cocompact subgroups of the planar Euclidean motion group E_2, counted up to affine equivalence. Discreteness is encoded as a properly discontinuous action on ℝ² — local finiteness of the return set at each point — equivalent on subgroups of E_d to Knill's positive-minimal-distance formulation, and avoids equipping E d ≃ᵃⁱ[ℝ] E d with a topology (mathlib has no default topology on the affine-isometry equiv type). Cocompactness is encoded as containing d linearly independent translations. §94 of Knill's Some Fundamental Theorems in Mathematics.

Formal statement

/-- **There are exactly 17 wallpaper groups** (Pólya–Niggli 1924). -/
theorem there_are_17_wallpaper_groups :
    crystallographicCount 2 = 17 := by
  sorry

Informal solution sketch

The classification proceeds in four steps. (1) Bieberbach's first theorem (1910): every crystallographic group G in dimension d contains a finite-index translation subgroup of rank d (the translation lattice Λ). (2) Point group: the quotient G / Λ embeds into O(d) and is finite; in dimension 2 it is one of the 10 finite subgroups {C₁, C₂, C₃, C₄, C₆, D₁, D₂, D₃, D₄, D₆} compatible with the crystallographic restriction (rotation orders ∈ {1, 2, 3, 4, 6}; orders 5 and ≥ 7 are excluded by the trace-rationality argument). (3) Extension classification: enumerate group extensions of each point group by each lattice it can preserve, classifying the relevant extensions via cocycles in group cohomology (H²(point group, Λ)) modulo affine conjugacy. (4) Compatibility: of the 17 candidate extensions, all 17 are realised by explicit examples (p1, p2, pm, pg, cm, pmm, pmg, pgg, cmm, p4, p4m, p4g, p3, p31m, p3m1, p6, p6m). Mathlib has EuclideanSpace, AffineIsometryEquiv, AffineEquiv, LinearIndependent, and IsOfFinOrder, but no wallpaper-group framework, no Bieberbach theorems, no point-group classification, no crystallographic-restriction theorem, no extension-cohomology classification in this dimension.

Source

G. Pólya, 'Über die Analogie der Kristallsymmetrie in der Ebene', Z. Kristallogr. 60 (1924) 278–282; P. Niggli, 'Die Flächensymmetrien homogener Diskontinuen', Z. Kristallogr. 60 (1924) 283–298. Listed as §94 in O. Knill, Some Fundamental Theorems in Mathematics (https://people.math.harvard.edu/~knill/graphgeometry/papers/fundamental.pdf).

How to submit

Challenge.lean and Solution.lean are part of the trusted benchmark and must not be modified. Write your proof in Submission.lean (plus any local modules under Submission/). Mathlib may be used freely; anything not in Mathlib has to be inlined into the submission.

Comparator configuration

• Solution module: Solution
• Theorems checked: there_are_17_wallpaper_groups
• Permitted axioms: propext, Quot.sound, Classical.choice

Submitted by Kim Morrison.