orbitCount_pos
plain-language theorem explainer
Every wallpaper symmetry group has a strictly positive canonical orbit count under its action. Workers deriving J-cost preferences from crystallographic symmetries cite this to guarantee positive ratios before applying the J functional. The argument is a one-line wrapper that cases on all seventeen group constructors, unfolds the explicit orbit assignment, and confirms each natural number is positive.
Claim. For every wallpaper group $g$, the canonical orbit count satisfies $0 < orbitCount(g)$.
background
WallpaperGroup is the inductive enumeration of the seventeen crystallographic plane symmetry groups in IUC notation, ordered to match Schattschneider 1978 and standard tables. orbitCount is the sibling definition that maps each constructor to its standard orbit multiplicity: 1 for p1, 2 for p2/pm/pg/cm, and so on up to 12 for p6m. The module replaces a v4 skeleton by defining wallpaperJ g as Cost.Jcost of the ratio orbitCount g over maxOrbitCount, so that J-cost lives on the positive reals and is reciprocal-symmetric.
proof idea
One-line wrapper that introduces the arbitrary group g, performs exhaustive case analysis on the seventeen constructors of WallpaperGroup, unfolds orbitCount to a concrete natural number in each branch, and applies norm_num to verify strict positivity.
why it matters
orbitCount_pos is invoked directly by symmetryGroupPreferenceCert (as orbit_pos) and by symmetryRatio_pos (via exact_mod_cast to obtain a positive real numerator). It supplies the lower bound required to form well-defined positive ratios and to prove wallpaperJ non-negative with its global minimum at p6m, closing the basic interface for the aesthetics track that replaces the v4 skeleton.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.