wallpaperJ_mono_in_orbits
plain-language theorem explainer
Wallpaper J-cost decreases as orbit count increases among the 17 wallpaper groups: if orbitCount g is at most orbitCount h then wallpaperJ h is at most wallpaperJ g. Researchers modeling symmetry preference in crystallography or aesthetics would cite this ordering. The proof reduces the claim to the known anti-monotonicity of J-cost on the unit interval by rewriting the symmetry ratio and comparing the resulting real inequalities.
Claim. For wallpaper groups $g,h$, if $orbitCount(g) ≤ orbitCount(h)$ then $J(orbitCount(h)/12) ≤ J(orbitCount(g)/12)$, where $J$ is the J-cost function and $12$ is the maximum orbit count.
background
The module enumerates the 17 wallpaper groups as the inductive type WallpaperGroup. For each group $g$, orbitCount $g$ records the canonical orbit multiplicity under the full symmetry action on the unit cell, with values ranging from 1 (p1) to 12 (p6m). maxOrbitCount is the constant 12, and symmetryRatio $g$ is the real quotient orbitCount $g$ / 12, which lies in the interval (0,1].
proof idea
The proof unfolds wallpaperJ to expose J-cost of the two symmetry ratios, then applies Jcost_anti_mono_on_unit_interval. It supplies positivity of both ratios via symmetryRatio_pos, the upper bound symmetryRatio_le_one on the larger ratio, and the key comparison symmetryRatio g ≤ symmetryRatio h. The comparison is obtained by rewriting div_le_div_iff, casting the integer hypothesis to reals, and closing with nlinarith.
why it matters
The result is invoked by preference_anti_mono_in_orbits to obtain the corresponding statement for the negated preference functional and by symmetry_group_preference_one_statement to assemble the three-part ordering (p6m at zero cost, p1 strictly positive, and monotonicity). It supplies the structural content for the aesthetic preference functional in the SymmetryGroupPreference module, confirming that higher symmetry yields lower J-cost.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.