WallpaperGroup
plain-language theorem explainer
The declaration enumerates the seventeen crystallographic wallpaper groups as an inductive type in IUC notation. Researchers applying J-cost to symmetry preferences in visual aesthetics cite this enumeration to index orbit multiplicities. The definition lists the groups in the order matching Schattschneider 1978 and standard tables, with no lemmas or tactics required.
Claim. The inductive type enumerating the seventeen wallpaper groups: $p1, p2, pm, pg, cm, pmm, pmg, pgg, cmm, p4, p4m, p4g, p3, p3m1, p31m, p6, p6m$.
background
The module develops visual symmetry-group preference (track A5/E5) by replacing an earlier skeleton definition of wallpaper J-cost. It now uses the genuine Cost.Jcost applied to the ratio of canonical orbit counts relative to the maximum. The WallpaperGroup type supplies the domain for orbitCount, which records the standard crystallographic multiplicities (p1 has one orbit, p6m has twelve). Upstream results supply foundational structures from PrimitiveDistinction.from (seven axioms to four conditions) and UniversalForcingSelfReference.for (meta-realization certificates), together with PhiLadderLattice.that (Poisson summation on the phi-ladder) and interval numerics.
proof idea
This is an inductive definition whose seventeen constructors directly list the groups. No lemmas are invoked and no tactics are applied; the declaration simply records the standard enumeration.
why it matters
The type is the base for orbitCount, symmetryRatio, preference, and the theorem preference_p6m_max, which establishes p6m as the J-cost minimum. It supplies the structural content for the cross-cultural preference result in the Recognition Science framework, linking J-uniqueness and the eight-tick octave to aesthetic ordering. The module doc-comment identifies the headline theorems wallpaperJ_p6m_eq_zero and preference_p6m_max that rest on this enumeration.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.