symmetry_group_preference_one_statement
plain-language theorem explainer
Researchers in symmetry-based aesthetics cite this result to establish that J-cost orders wallpaper groups by decreasing symmetry. It asserts that p6m achieves J-cost zero, p1 has strictly positive J-cost, and any increase in orbit count strictly lowers J-cost. The proof is a one-line term that packages the three component theorems wallpaperJ_p6m_eq_zero, wallpaperJ_p1_pos, and wallpaperJ_mono_in_orbits.
Claim. $J(p_{6m})=0$ and $0<J(p_1)$ and, for wallpaper groups $g,h$, if orbit count $n(g)≤n(h)$ then $J(h)≤J(g)$, where $J(g)$ is the J-cost of the ratio $n(g)/12$.
background
The module enumerates the seventeen wallpaper groups by their canonical orbit multiplicities under the full symmetry action. orbitCount assigns the standard crystallographic values (p1 has 1, p6m has 12). wallpaperJ is defined as Cost.Jcost applied to the symmetry ratio orbitCount(g)/maxOrbitCount, which is the genuine J-cost of the orbit-multiplicity ratio on the unit interval. This replaces the earlier placeholder that simply used raw orbit count. The local setting is Track A5/E5, deriving visual symmetry preference directly from the J-cost functional.
proof idea
The proof is a term-mode conjunction that directly supplies the three upstream results: wallpaperJ_p6m_eq_zero (which reduces to Cost.Jcost_unit0 after unfolding symmetryRatio_p6m), wallpaperJ_p1_pos (which applies wallpaperJ_pos_of_ne_one and norm_num on the ratio 1/12), and wallpaperJ_mono_in_orbits (which invokes Jcost_anti_mono_on_unit_interval after confirming positivity of the ratios).
why it matters
The declaration supplies the structural content for cross-cultural preference ordering under the J-cost-derived functional. It shows that maximum-symmetry groups are universally preferred because J reaches its global minimum of zero precisely when the ratio equals 1 and is strictly monotonic in orbit count. This fills the headline theorem slot in the Aesthetics module and connects to the J-uniqueness property (T5) and the fixed-point forcing of phi in the UnifiedForcingChain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.