preference_p6m_eq_zero
plain-language theorem explainer
The theorem shows that the aesthetic preference functional evaluates to zero at the p6m wallpaper group. Researchers working on symmetry-derived aesthetics or Recognition Science derivations would cite it to locate the J-cost minimum. The proof is a direct term reduction that unfolds the preference definition, substitutes the prior zero result for wallpaperJ at p6m, and closes with ring arithmetic.
Claim. $preference(p_{6m}) = 0$, where $preference(g) := -J(orbitCount(g)/12)$ and $J$ denotes the J-cost of the orbit-multiplicity ratio relative to the maximum of 12.
background
The module defines wallpaper J-cost as the genuine Cost.Jcost applied to the ratio of a group's canonical orbit count to the maximum (12 for p6m). Preference is then the negation of this J-cost, so that lower cost yields higher preference. Upstream results establish that J vanishes exactly when the ratio equals 1 and that J is nonnegative everywhere, with the p6m case following from symmetryRatio_p6m together with Cost.Jcost_unit0.
proof idea
The proof is a one-line term wrapper. It unfolds the definition of preference, rewrites the resulting wallpaperJ(.p6m) term by the already-proved wallpaperJ_p6m_eq_zero lemma, and finishes with the ring tactic on the resulting -0 expression.
why it matters
This pins the zero of the preference functional at maximal symmetry, supplying the base case for the claim that p6m is universally maximally preferred. It completes the structural replacement of the earlier skeleton definition and ties the aesthetic ordering to the J-cost minimum at the self-similar fixed point in the Recognition framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.