orbitCount_le_max
plain-language theorem explainer
The theorem establishes that the canonical orbit count for any wallpaper group is at most twelve, the value attained by p6m. Researchers deriving J-cost orderings for visual symmetries cite this bound when constructing the symmetry ratio that enters wallpaperJ. The proof is a one-line wrapper performing exhaustive case analysis on the WallpaperGroup inductive type followed by numerical normalization.
Claim. For every wallpaper group $g$, the canonical orbit multiplicity of $g$ satisfies $orbitCount(g) ≤ 12$, where 12 is the multiplicity of the group p6m.
background
The module replaces an earlier skeleton by enumerating the seventeen wallpaper groups and defining wallpaperJ as the J-cost of the orbit-multiplicity ratio. WallpaperGroup is the inductive type listing the IUC groups p1 through p6m. orbitCount maps each group to its standard crystallographic orbit cardinality under the full symmetry action, while maxOrbitCount is the constant 12 attained by p6m. This bound is required to form the symmetry ratio orbitCount g / maxOrbitCount, which is then fed to Cost.Jcost.
proof idea
The proof performs case analysis on the inductive WallpaperGroup type. For each of the seventeen constructors it unfolds orbitCount and maxOrbitCount, then applies norm_num to discharge the resulting numerical inequality.
why it matters
The lemma supplies the inequality used by symmetryRatio_le_one to prove that the symmetry ratio is at most one. It supports the headline claim that p6m achieves the global J-cost minimum among wallpaper groups, consistent with Recognition Science preference for maximal symmetry. The result closes an explicit enumeration step in the aesthetics track.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.