pith. machine review for the scientific record. sign in
def definition def or abbrev high

preference

show as:
view Lean formalization →

The preference functional assigns to each wallpaper group the negation of its J-cost on the symmetry ratio, so that higher symmetry yields higher preference. Researchers modeling cross-cultural pattern preference would cite this definition to derive rankings directly from the Recognition Science cost functional. It is a one-line wrapper that negates the output of wallpaperJ.

claimFor a wallpaper group $g$, the preference is defined by $P(g) = -J(r(g))$, where $r(g)$ is the ratio of the canonical orbit count of $g$ to the maximum orbit count (equal to 12) and $J$ denotes the J-cost function.

background

This definition sits inside the module on visual symmetry-group preference, which replaces an earlier placeholder that used raw orbit counts. WallpaperGroup is the inductive enumeration of the seventeen crystallographic wallpaper groups in IUC notation. The symmetry ratio of a group is its orbit count divided by the maximum (the orbit count of p6m). wallpaperJ applies Cost.Jcost to this ratio, producing a non-negative real number that vanishes exactly when the ratio equals one.

proof idea

One-line wrapper that applies negation to the value of wallpaperJ g.

why it matters in Recognition Science

The definition supplies the preference functional used to prove that p6m is the unique maximum and that preference is anti-monotone in orbit count. It directly feeds the downstream theorems preference_p6m_max, preference_anti_mono_in_orbits, and the master certificate SymmetryGroupPreferenceCert. Within the Recognition framework it realizes the J-cost minimum at maximal symmetry (T5 J-uniqueness), furnishing a concrete, hypothesis-free prediction for cross-cultural aesthetic preference.

scope and limits

formal statement (Lean)

 260def preference (g : WallpaperGroup) : ℝ := - wallpaperJ g

proof body

Definition body.

 261

used by (17)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (2)

Lean names referenced from this declaration's body.