English
If a cost function f has the Max-Cut property at a,b and ω is a symmetric fractional operation, then for any r in the transformed ω.tt set corresponding to a,b, f at [a,b] is strictly less than f(r).
Русский
Если f имеет свойство Max-Cut на парах a,b, а ω симметричная фракционная операция, то для любого r из ω.tt на паре [a,b], значение f на [a,b] строго меньше, чем на r.
LaTeX
$$$\\text{Rows}(f,a,b) \\to \\; f([a,b]) < f(r)$ для каждого r в соответствующей ω.tt-обработке$$
Lean4
theorem rows_lt_aux {C : Type*} [PartialOrder C] {f : (Fin 2 → D) → C} {a b : D} (mcf : f.HasMaxCutPropertyAt a b)
(hab : a ≠ b) {ω : FractionalOperation D 2} (symmega : ω.IsSymmetric) {r : Fin 2 → D}
(rin : r ∈ (ω.tt ![![a, b], ![b, a]])) : f ![a, b] < f r :=
by
rw [FractionalOperation.tt, Multiset.mem_map] at rin
rw [show r = ![r 0, r 1] by simp [← List.ofFn_inj]]
apply lt_of_le_of_ne (mcf.right (r 0) (r 1)).left
intro equ
have asymm : r 0 ≠ r 1 :=
by
rcases (mcf.right (r 0) (r 1)).right equ with ⟨ha0, hb1⟩ | ⟨ha1, hb0⟩
· rw [ha0, hb1] at hab
exact hab
· rw [ha1, hb0] at hab
exact hab.symm
apply asymm
obtain ⟨o, in_omega, rfl⟩ := rin
change o (fun j => ![![a, b], ![b, a]] j 0) = o (fun j => ![![a, b], ![b, a]] j 1)
convert symmega ![a, b] ![b, a] (by simp [List.Perm.swap]) o in_omega using 2 <;> simp [Matrix.const_fin1_eq]
