wallpaperJ_p6m_le
plain-language theorem explainer
The theorem establishes that p6m attains the global minimum J-cost among the seventeen wallpaper groups. Researchers deriving symmetry preferences from Recognition Science cost functionals would cite it to order crystallographic groups by orbit-multiplicity ratios. The proof is a direct one-line reduction that substitutes the zero value for p6m and invokes non-negativity of J-cost for the remaining groups.
Claim. Let $J(g)$ denote the J-cost of the orbit-multiplicity ratio of wallpaper group $g$. Then $J(p6m) ≤ J(g)$ for every wallpaper group $g$.
background
The module defines wallpaper J-cost via the genuine Cost.Jcost applied to symmetry ratios. WallpaperGroup enumerates the seventeen crystallographic groups in IUC order. For each $g$, orbitCount $g$ records the canonical orbit multiplicity under the full group action, with maxOrbitCount equal to 12 for p6m. Thus wallpaperJ $g$ equals Cost.Jcost of (orbitCount $g$ / 12), which lies in (0,1] and satisfies the reciprocal symmetry of the J function. Upstream results supply wallpaperJ_p6m_eq_zero, which places p6m at J=0, and wallpaperJ_nonneg, which asserts non-negativity for arbitrary $g$ from Cost.Jcost_nonneg.
proof idea
The proof is a one-line wrapper. It rewrites the left-hand side to zero by wallpaperJ_p6m_eq_zero, then applies wallpaperJ_nonneg $g$ to obtain the inequality.
why it matters
This lemma supplies the non-strict minimality of p6m that underpins the aesthetics track claim of symmetry preference. It directly feeds the headline result that p6m is the universally preferred wallpaper group under the J-cost ordering. The construction replaces the v4 placeholder orbit-count cost with the genuine Cost.Jcost on the ratio, aligning with the Recognition Science derivation of J from the forcing chain and the RCL identity. No open scaffolding remains for this ordering step.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.