Jcost_anti_mono_on_unit_interval
plain-language theorem explainer
J-cost decreases as the ratio increases toward 1 on (0,1]. Symmetry preference models cite this to rank wallpaper groups by orbit count. The tactic proof rewrites both sides via the squared form of J-cost, clears denominators, substitutes a=1-x and b=1-y, and chains two product inequalities using nonnegativity of squares together with x ≤ y.
Claim. For real numbers $x,y$ with $0<x≤y≤1$, $J(y)≤J(x)$ where $J(t)=(t-1)^2/(2t)$ for $t>0$.
background
J-cost is the function $J(x)=(x+x^{-1})/2-1$ on positive reals, equivalently $(x-1)^2/(2x)$ by the upstream lemma Jcost_eq_sq. The Aesthetics module defines wallpaperJ g as J of the ratio orbitCount g over maxOrbitCount=12, so that wallpaperJ measures deviation of a symmetry group's orbit multiplicity from the p6m maximum. Preference is defined as the negation of wallpaperJ. This theorem supplies the monotonicity on the unit interval that converts orbit-count ordering into J-cost ordering.
proof idea
Apply Jcost_eq_sq to both sides. Clear the positive denominators with div_le_div_iff0. Set a=1-x≥0 and b=1-y≥0 so that b≤a. Rewrite the squared terms, obtain b²≤a² from mul_self_le_mul_self, then split the target product inequality into b²·(2x)≤a²·(2x) followed by a²·(2x)≤a²·(2y) and finish with linarith.
why it matters
wallpaperJ_mono_in_orbits invokes this result to conclude that higher orbit count yields strictly lower wallpaperJ and therefore higher preference. It supplies the anti-monotonicity step required for the full ordering of the seventeen wallpaper groups under the J-cost preference functional. In the Recognition framework it realizes the concrete consequence of J-uniqueness (T5) on the interval of ratios below the self-similar fixed point.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.