maxOrbitCount
plain-language theorem explainer
maxOrbitCount is the constant 12 serving as the orbit cardinality of the p6m wallpaper group. Researchers deriving J-cost preferences for the seventeen wallpaper groups cite it to normalize symmetry ratios in (0,1]. The definition is a direct numeric assignment with no computation or lemmas.
Claim. Let $M := 12$ denote the orbit cardinality of the p6m wallpaper group, used to normalize the symmetry ratio $r_g = o_g / M$ for each wallpaper group $g$ where $o_g$ is its canonical orbit count.
background
The Aesthetics module enumerates the seventeen wallpaper groups by canonical orbit multiplicity under the full symmetry action. Wallpaper J-cost is defined as Cost.Jcost of the ratio (orbitCount g / maxOrbitCount), placing the ratio on the positive reals where J is reciprocal-symmetric. maxOrbitCount fixes the denominator so that p6m achieves ratio 1 and thus J-cost zero. The module replaces an earlier skeleton by grounding the cost in the genuine Cost.Jcost rather than raw integer orbit counts. This constant appears directly in the SymmetryGroupPreferenceCert structure that collects the eight clauses for the cross-cultural preference prediction.
proof idea
Direct constant definition assigning the value 12. No lemmas or tactics are invoked; the declaration serves as the base value referenced by orbitCount_p6m and orbitCount_le_max.
why it matters
This supplies the normalization factor for all symmetry ratios in the wallpaper J-cost construction. It is referenced by SymmetryGroupPreferenceCert (which records orbit_p6m_eq_max and ratio_le_one) and by preference_anti_mono_in_orbits. In the Recognition framework it supports the ordering that favors higher-symmetry groups, consistent with J-uniqueness and the forcing chain. The parent results include wallpaperJ_p6m_eq_zero and the headline preference theorems listed in the module documentation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.