`preference`

definition

show as: view math explainer →

module: IndisputableMonolith.Aesthetics.SymmetryGroupPreference
domain: Aesthetics
line: 260 · github
papers citing: none yet

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.Aesthetics.SymmetryGroupPreference on GitHub at line 260.

browse module

All declarations in this module, on Recognition.

explainer page

A cached Ask Recognition explainer exists for this declaration.

open explainer

depends on

used by

formal source

 257
 258/-- Aesthetic preference is the negation of J-cost: higher preference =
 259lower cost. -/
 260def preference (g : WallpaperGroup) : ℝ := - wallpaperJ g
 261
 262theorem preference_p6m_eq_zero : preference .p6m = 0 := by
 263  unfold preference
 264  rw [wallpaperJ_p6m_eq_zero]
 265  ring
 266
 267/-- **THEOREM.** `p6m` is the universally maximally preferred
 268wallpaper group under the J-cost-derived preference functional. -/
 269theorem preference_p6m_max (g : WallpaperGroup) :
 270    preference g ≤ preference .p6m := by
 271  unfold preference
 272  rw [wallpaperJ_p6m_eq_zero]
 273  have := wallpaperJ_nonneg g
 274  linarith
 275
 276/-- Anti-monotone in orbits: if `orbitCount g ≤ orbitCount h`, then
 277preference for `g` is at most preference for `h`. -/
 278theorem preference_anti_mono_in_orbits {g h : WallpaperGroup}
 279    (hgh : orbitCount g ≤ orbitCount h) :
 280    preference g ≤ preference h := by
 281  unfold preference
 282  have := wallpaperJ_mono_in_orbits hgh
 283  linarith
 284
 285/-! ## §5. Master certificate -/
 286
 287/-- **SYMMETRY GROUP PREFERENCE MASTER CERTIFICATE.** Eight clauses
 288backing the J-cost-driven cross-cultural preference prediction. All
 289fields derived from `Cost.Jcost`, not asserted as orbit-count
 290arithmetic.

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.