pith. machine review for the scientific record. sign in
theorem proved term proof

preference_anti_mono_in_orbits

show as:
view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

formal statement (Lean)

 278theorem preference_anti_mono_in_orbits {g h : WallpaperGroup}
 279    (hgh : orbitCount g ≤ orbitCount h) :
 280    preference g ≤ preference h := by

proof body

Term-mode proof.

 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.
 291
 2921. `orbit_pos`: every group has positive orbit count.
 2932. `orbit_p6m_eq_max`: `p6m` orbit count = 12 = `maxOrbitCount`.
 2943. `ratio_le_one`: every symmetry ratio is in `(0, 1]`.
 2954. `J_nonneg`: every wallpaper J-cost is non-negative.
 2965. `J_p6m_zero`: `p6m` sits at the J-cost floor.
 2976. `J_p1_pos`: `p1` has strictly positive J-cost.
 2987. `J_mono`: J-cost is anti-monotone in orbit count.
 2998. `preference_p6m_max`: `p6m` maximizes preference.
 300-/

depends on (16)

Lean names referenced from this declaration's body.