wallpaperJ_p6m_eq_zero
plain-language theorem explainer
p6m achieves the minimum J-cost of zero among the seventeen wallpaper groups because its orbit-multiplicity ratio equals unity. Researchers working on symmetry-derived preference functionals in Recognition Science aesthetics would cite this to anchor the ordering that places maximal symmetry at the cost floor. The proof is a direct one-line reduction that substitutes the ratio via symmetryRatio_p6m and invokes the base lemma Jcost 1 = 0.
Claim. The J-cost of the p6m wallpaper group equals zero: $J(r) = 0$ where $r$ is the symmetry ratio (orbit count of p6m divided by the maximum orbit count of 12).
background
The module enumerates the seventeen wallpaper groups by canonical orbit cardinality under the full symmetry action and defines wallpaperJ(g) as Cost.Jcost applied to the symmetry ratio (orbitCount(g) normalized by maxOrbitCount = 12). This replaces the v4 placeholder that used raw orbit count. The local theoretical setting is the aesthetics track (A5/E5) that derives visual symmetry preference from J-cost minimization, with p6m as the structural maximum-symmetry case.
proof idea
The term proof unfolds the definition of wallpaperJ, rewrites the symmetry ratio of p6m to exactly 1 using the upstream theorem symmetryRatio_p6m, and applies the lemma Jcost_unit0 that states Jcost(1) = 0.
why it matters
This result is invoked directly by preference_p6m_eq_zero, preference_p6m_max, symmetryGroupPreferenceCert, symmetry_group_preference_one_statement, and wallpaperJ_p6m_le. It supplies the headline claim in the module that p6m sits at the J-cost floor, which forces the universal preference ordering p6m ≻ all other groups under the J-cost functional. In the broader framework it closes the base case for the anti-monotonicity of J-cost on symmetry ratios in [1/12, 1].
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.