preference_p6m_max
plain-language theorem explainer
p6m achieves the global maximum of the preference functional among the seventeen wallpaper groups. Researchers studying symmetry-driven aesthetics or cross-cultural pattern preference would cite this result. The proof is a one-line wrapper that unfolds preference to negation of wallpaperJ, substitutes the zero J-cost at p6m, invokes non-negativity of J-cost for arbitrary groups, and concludes via linear arithmetic.
Claim. For every wallpaper group $g$, the preference of $g$ satisfies preference$(g) ≤$ preference$(p6m)$, where preference$(g) := -$Jcost$(orbitCount(g)/maxOrbitCount)$ and maxOrbitCount equals the orbit count of $p6m$.
background
The module enumerates the seventeen wallpaper groups in IUC notation and defines orbitCount as the canonical orbit multiplicity under the full symmetry action (p1 has 1, p6m has 12). wallpaperJ is then Cost.Jcost of the ratio orbitCount(g)/maxOrbitCount, which is reciprocal-symmetric and non-negative. preference is defined as the negation of wallpaperJ, so higher preference corresponds to lower J-cost. Upstream results establish that wallpaperJ p6m equals zero (by symmetryRatio_p6m and Cost.Jcost_unit0) and that wallpaperJ g is nonnegative for every g (by Cost.Jcost_nonneg).
proof idea
Unfold the definition of preference to obtain -wallpaperJ g ≤ -wallpaperJ p6m. Rewrite the right-hand side using wallpaperJ_p6m_eq_zero to replace wallpaperJ p6m with zero. Apply wallpaperJ_nonneg g to obtain 0 ≤ wallpaperJ g. Linear arithmetic then yields the desired inequality.
why it matters
This theorem certifies p6m as the unique maximum-preference wallpaper group under the J-cost model and supplies the key clause J_p6m_zero inside the SymmetryGroupPreferenceCert structure. It is invoked by preference_anti_mono_in_orbits to establish the full anti-monotonicity ordering and completes the structural content for the cross-cultural preference prediction in the Aesthetics track. The result aligns with the Recognition Science emphasis on J-cost minimization at maximal symmetry (T5 J-uniqueness) without invoking additional hypotheses.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.