wallpaperJ_pos_of_ne_one
plain-language theorem explainer
For any wallpaper group whose orbit-count ratio to the p6m maximum differs from one, the associated J-cost is strictly positive. Researchers ordering crystallographic patterns by recognition cost or deriving visual symmetry preferences cite this result. The proof unfolds the J-cost definition, rewrites it via the squared-difference identity, confirms the ratio is positive and nonzero, then applies the positivity tactic to the resulting fraction.
Claim. Let $g$ be any of the seventeen wallpaper groups and let $r = $ orbitCount$(g)/$maxOrbitCount$ be its symmetry ratio. If $r ≠ 1$ then $0 < $ Jcost$(r)$, where Jcost$(x) = (x-1)^2/(2x)$.
background
The module enumerates the seventeen wallpaper groups by canonical orbit multiplicity under the full symmetry action and replaces an earlier placeholder definition with the genuine Cost.Jcost applied to the ratio. WallpaperGroup is the inductive type listing p1 through p6m in IUC order. symmetryRatio g is defined as (orbitCount g : ℝ) / (maxOrbitCount : ℝ) with maxOrbitCount equal to the p6m value 12, so the ratio lies in (0,1]. wallpaperJ g is then Cost.Jcost of that ratio. The upstream lemma Jcost_eq_sq supplies the algebraic identity Jcost x = (x-1)^2 / (2x) for x ≠ 0, while symmetryRatio_pos guarantees the ratio is always positive.
proof idea
Unfold wallpaperJ to Cost.Jcost (symmetryRatio g). Apply symmetryRatio_pos to obtain 0 < symmetryRatio g, then ne_of_gt to obtain the nonzero hypothesis needed for Jcost_eq_sq. Rewrite the cost via that lemma. From the assumption symmetryRatio g ≠ 1 derive (symmetryRatio g - 1) ≠ 0 by sub_ne_zero, hence the squared numerator is positive by positivity. The denominator 2 * symmetryRatio g is positive by linarith. Finish with the positivity tactic on the resulting positive-over-positive expression.
why it matters
The result is invoked directly by wallpaperJ_p1_pos to establish strict positivity for the trivial-symmetry group p1. It supplies one of the headline facts listed in the module doc-comment that together show p6m achieves the global J-cost minimum and that higher-orbit groups are preferred. The construction sits inside the Recognition Science aesthetics track and inherits the J-cost functional whose uniqueness is fixed at T5 of the forcing chain; the positivity statement is the concrete obstruction that prevents any non-maximal group from being cost-minimal.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.