preference_anti_mono_in_orbits
plain-language theorem explainer
Wallpaper groups with non-decreasing orbit counts under the canonical action have non-decreasing J-cost-derived preference. Researchers modeling visual symmetry preferences or cross-cultural aesthetics would cite the ordering to rank groups without recomputing costs. The proof is a direct reduction that unfolds preference to the negation of wallpaperJ and applies the established anti-monotonicity of J-cost on the unit interval together with linear arithmetic.
Claim. Let $g,h$ be wallpaper groups. If the canonical orbit count of $g$ is at most that of $h$, then preference of $g$ is at most preference of $h$, where preference$(g) := -J(g)$ and $J(g) :=$ Cost.Jcost(orbitCount$(g)$/maxOrbitCount) with maxOrbitCount $=12$.
background
The module enumerates the seventeen wallpaper groups and replaces an earlier orbit-count placeholder with the genuine Cost.Jcost applied to the ratio orbitCount$(g)$/maxOrbitCount. Here maxOrbitCount is the orbit cardinality of p6m, equal to 12. Preference is defined as the negation of this wallpaperJ, so that lower J-cost corresponds to higher aesthetic preference. The upstream result wallpaperJ_mono_in_orbits establishes the corresponding anti-monotonicity for J itself: if orbitCount $g$ ≤ orbitCount $h$ then wallpaperJ $h$ ≤ wallpaperJ $g$, using Jcost_anti_mono_on_unit_interval and symmetryRatio_pos.
proof idea
Unfold the definition of preference to obtain the negation of wallpaperJ. Apply the upstream theorem wallpaperJ_mono_in_orbits directly to the given orbit-count hypothesis. Finish with linarith to reverse the inequality under negation.
why it matters
The declaration supplies the preference form of the J-mono clause in the symmetry-group preference master certificate. It guarantees that p6m, which maximizes orbit count, also maximizes preference, and thereby closes one of the eight supporting statements for the J-cost-driven ordering. The result sits inside the Recognition framework's use of Cost.Jcost on ratios that are reciprocal-symmetric, consistent with the Recognition Composition Law, though the module itself remains within the two-dimensional wallpaper setting.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.