orbitCount_p6m
plain-language theorem explainer
The theorem states that the p6m wallpaper group attains the maximum canonical orbit count of twelve among the seventeen wallpaper groups. Researchers deriving J-cost preferences for visual symmetries cite it to anchor the zero-cost point at maximal symmetry. The proof is a one-line term wrapper that unfolds the two definitions and closes by reflexivity.
Claim. $orbitCount(p6m) = maxOrbitCount$, where $maxOrbitCount = 12$ is the orbit multiplicity of the highest-symmetry wallpaper group under the full symmetry-group action on the unit cell.
background
The Aesthetics.SymmetryGroupPreference module enumerates the seventeen wallpaper groups by their canonical generator-orbit multiplicities. The definition orbitCount assigns to each WallpaperGroup its standard crystallographic orbit count under the full symmetry-group action, with p1 having one orbit and p6m having twelve. These counts are the point-group order times one for symmorphic groups, inherited from the point group for non-symmorphic cases on a suitable fundamental domain.
proof idea
The proof is a one-line term-mode wrapper. It unfolds orbitCount and maxOrbitCount; reflexivity then closes the goal because maxOrbitCount is defined to be exactly the value assigned to p6m by orbitCount.
why it matters
This result is invoked by symmetryGroupPreferenceCert to certify the full preference ordering and by symmetryRatio_p6m to obtain the ratio value 1 for p6m. It supplies the concrete anchor that places the J-cost minimum at maximal symmetry, consistent with the Recognition Science preference for the self-similar fixed point and the reciprocal symmetry of J. No open scaffolding remains at this step.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.