orbitCount
plain-language theorem explainer
orbitCount assigns the standard crystallographic orbit multiplicities to each of the seventeen wallpaper groups, with p1 at 1 and p6m at 12. Researchers working on J-cost symmetry preference in Recognition Science cite these values to form the ratios that enter wallpaperJ. The definition is implemented by exhaustive pattern matching on the WallpaperGroup inductive constructors.
Claim. Let $G$ be the inductive type of the seventeen wallpaper groups. The function $orbitCount : G → ℕ$ returns the orbit cardinality under the full group action on the unit cell, with values 1 for p1, 2 for p2/pm/pg/cm, 4 for pmm/pmg/pgg/cmm/p4, 8 for p4m/p4g, 3 for p3, 6 for p3m1/p31m/p6, and 12 for p6m.
background
The module Aesthetics.SymmetryGroupPreference replaces the v4 skeleton by defining wallpaper J-cost as the genuine Cost.Jcost of the orbit-multiplicity ratio. WallpaperGroup is the inductive type enumerating the seventeen crystallographic wallpaper groups in IUC notation, matching Schattschneider 1978. From the module documentation: 'For each of the seventeen wallpaper groups we record orbitCount g, the orbit cardinality of the canonical fundamental domain under the full symmetry group action (the standard crystallographic count: p1 has 1 orbit, p6m has 12, etc.).' orbitCount supplies the numerator for the ratio in wallpaperJ g := Cost.Jcost (orbitCount g / maxOrbitCount), where maxOrbitCount equals 12.
proof idea
The definition proceeds by exhaustive case analysis on the WallpaperGroup inductive type, directly assigning the listed integer multiplicities to each constructor.
why it matters
This definition supplies the integer data used by downstream results including orbitCount_p6m, orbitCount_le_max, preference_anti_mono_in_orbits, preference_p6m_max, and the SymmetryGroupPreferenceCert structure. It fills the enumeration step that lets wallpaperJ reach its minimum of zero at p6m, supporting the claim that maximum symmetry is preferred under the J-cost functional. The construction aligns with the Recognition Science derivation of preference orderings from the J-cost minimum at ratio 1.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.