Independent local improvements of all threshold cuts

Changing the keys at an independent set of vertices to the medians of their neighbours cannot increase any threshold cut. Independence matters: simultaneous majority updates at adjacent vertices need not improve a cut. The exact accounting identity also records the gain needed for a probabilistic improvement of the Gaussian layout constant.

def Complexity.Frontier.Multigraph.crossing {V : Type u_1} {E : Type u_2} (G : Multigraph V E) (c : V → Bool) (e : E) : ℕ

Indicator that the endpoints receive different colours.

Equations

• G.crossing c e = if c (G.src e) = c (G.tgt e) then 0 else 1

def Complexity.Frontier.Multigraph.cutSize {V : Type u_1} {E : Type u_2} [Fintype E] (G : Multigraph V E) (c : V → Bool) : ℕ

Number of edges crossing a Boolean cut.

Equations

• G.cutSize c = ∑ e : E, G.crossing c e

theorem Complexity.Frontier.Multigraph.cutSize_eq_ncard {V : Type u_1} {E : Type u_2} [Fintype E] (G : Multigraph V E) (c : V → Bool) : G.cutSize c = (G.cut {v : V | c v = true}).ncard

The sum definition is the ordinary multigraph cut cardinality.

noncomputable def Complexity.Frontier.Multigraph.localCut {V : Type u_1} {E : Type u_2} [Fintype E] (G : Multigraph V E) (c : V → Bool) (v : V) : ℕ

Number of crossing edges incident to a vertex.

Equations

• G.localCut c v = ∑ e : E, if G.Incident v e then G.crossing c e else 0

theorem Complexity.Frontier.Multigraph.sum_incident_independent {V : Type u_1} {E : Type u_2} [Fintype E] (G : Multigraph V E) (I : Finset V) (hI : ∀ (e : E), ¬(G.src e ∈ I ∧ G.tgt e ∈ I)) (w : E → ℕ) : (∑ v ∈ I, ∑ e : E, if G.Incident v e then w e else 0) = ∑ e : E, if G.src e ∈ I ∨ G.tgt e ∈ I then w e else 0

Incident-edge costs are counted once when the selected vertices are independent.

theorem Complexity.Frontier.Multigraph.cutSize_add_local_eq {V : Type u_1} {E : Type u_2} [Fintype E] (G : Multigraph V E) (I : Finset V) (hI : ∀ (e : E), ¬(G.src e ∈ I ∧ G.tgt e ∈ I)) (c c' : V → Bool) (hfix : ∀ v ∉ I, c' v = c v) : G.cutSize c' + ∑ v ∈ I, G.localCut c v = G.cutSize c + ∑ v ∈ I, G.localCut c' v

Exact change in a cut after updating an independent set.

theorem Complexity.Frontier.Multigraph.cutSize_le_of_local {V : Type u_1} {E : Type u_2} [Fintype E] (G : Multigraph V E) (I : Finset V) (hI : ∀ (e : E), ¬(G.src e ∈ I ∧ G.tgt e ∈ I)) (c c' : V → Bool) (hfix : ∀ v ∉ I, c' v = c v) (hlocal : ∀ v ∈ I, G.localCut c' v ≤ G.localCut c v) : G.cutSize c' ≤ G.cutSize c

Independent local minimizers improve the entire cut.

theorem Complexity.Frontier.Multigraph.cutSize_lt_of_local {V : Type u_1} {E : Type u_2} [Fintype E] (G : Multigraph V E) (I : Finset V) (hI : ∀ (e : E), ¬(G.src e ∈ I ∧ G.tgt e ∈ I)) (c c' : V → Bool) (hfix : ∀ v ∉ I, c' v = c v) (hlocal : ∀ v ∈ I, G.localCut c' v ≤ G.localCut c v) (hstrict : ∃ v ∈ I, G.localCut c' v < G.localCut c v) : G.cutSize c' < G.cutSize c

theorem Complexity.Frontier.Multigraph.cutSize_eq_add_gain {V : Type u_1} {E : Type u_2} [Fintype E] (G : Multigraph V E) (I : Finset V) (hI : ∀ (e : E), ¬(G.src e ∈ I ∧ G.tgt e ∈ I)) (c c' : V → Bool) (hfix : ∀ v ∉ I, c' v = c v) (hlocal : ∀ v ∈ I, G.localCut c' v ≤ G.localCut c v) : G.cutSize c = G.cutSize c' + ∑ v ∈ I, (G.localCut c v - G.localCut c' v)

The gain is the sum of local gains, with no loss from overlapping updated stars.

noncomputable def Complexity.Frontier.Multigraph.otherEnd {V : Type u_1} {E : Type u_2} (G : Multigraph V E) (v : V) (e : E) : V

The other endpoint of an incident edge.

Equations

• G.otherEnd v e = if G.src e = v then G.tgt e else G.src e

theorem Complexity.Frontier.Multigraph.crossing_eq_otherEnd {V : Type u_1} {E : Type u_2} (G : Multigraph V E) (c : V → Bool) (v : V) {e : E} (he : G.Incident v e) : G.crossing c e = if c v = c (G.otherEnd v e) then 0 else 1

def Complexity.Frontier.LocalLayout.median3 (a b c : ℝ) : ℝ

The median of three keys, expressed using lattice operations.

Equations

• Complexity.Frontier.LocalLayout.median3 a b c = max (min a b) (min (max a b) c)

def Complexity.Frontier.LocalLayout.disagreements3 (c : Bool) (neighbours : Fin 3 → Bool) : ℕ

The number of the three neighbour colours that differ from c.

Equations

• Complexity.Frontier.LocalLayout.disagreements3 c neighbours = ∑ i : Fin 3, if c = neighbours i then 0 else 1

theorem Complexity.Frontier.LocalLayout.disagreements_median3_le (k : Fin 3 → ℝ) (t : ℝ) (c : Bool) : (disagreements3 (decide (median3 (k 0) (k 1) (k 2) < t)) fun (i : Fin 3) => decide (k i < t)) ≤ disagreements3 c fun (i : Fin 3) => decide (k i < t)

At every threshold, the median agrees with a majority of the neighbours.

theorem Complexity.Frontier.LocalLayout.localCut_eq_star {V : Type u_1} {E : Type u_2} [Fintype E] (G : Multigraph V E) (v : V) (edges : Fin 3 ≃ ↑(G.edgesAt v)) (c : V → Bool) : G.localCut c v = disagreements3 (c v) fun (i : Fin 3) => c (G.otherEnd v ↑(edges i))

Enumerating the three incident edges supplies exactly the star identity used below.

theorem Complexity.Frontier.LocalLayout.otherEnd_notMem {V : Type u_1} {E : Type u_2} (G : Multigraph V E) (I : Finset V) (hI : ∀ (e : E), ¬(G.src e ∈ I ∧ G.tgt e ∈ I)) {v : V} (hv : v ∈ I) {e : E} (he : G.Incident v e) : G.otherEnd v e ∉ I

Independence keeps every neighbour of an updated vertex fixed.

noncomputable def Complexity.Frontier.LocalLayout.improve {V : Type u_1} (I : Finset V) (neighbours : V → Fin 3 → V) (key : V → ℝ) : V → ℝ

Replace the selected keys by the medians of their three neighbour keys.

Equations

• One or more equations did not get rendered due to their size.

theorem Complexity.Frontier.LocalLayout.improve_of_mem {V : Type u_1} {I : Finset V} (neighbours : V → Fin 3 → V) (key : V → ℝ) {v : V} (hv : v ∈ I) : improve I neighbours key v = median3 (key (neighbours v 0)) (key (neighbours v 1)) (key (neighbours v 2))

theorem Complexity.Frontier.LocalLayout.improve_of_not_mem {V : Type u_1} {I : Finset V} (neighbours : V → Fin 3 → V) (key : V → ℝ) {v : V} (hv : v ∉ I) : improve I neighbours key v = key v

theorem Complexity.Frontier.LocalLayout.cutSize_improve_le {V : Type u_1} {E : Type u_2} [Fintype E] (G : Multigraph V E) (I : Finset V) (hI : ∀ (e : E), ¬(G.src e ∈ I ∧ G.tgt e ∈ I)) (neighbours : V → Fin 3 → V) (hstar : ∀ v ∈ I, ∀ (c : V → Bool), G.localCut c v = disagreements3 (c v) fun (i : Fin 3) => c (neighbours v i)) (hout : ∀ v ∈ I, ∀ (i : Fin 3), neighbours v i ∉ I) (key : V → ℝ) (t : ℝ) : (G.cutSize fun (v : V) => decide (improve I neighbours key v < t)) ≤ G.cutSize fun (v : V) => decide (key v < t)

All thresholds improve simultaneously. The star identity makes the three-neighbour representation explicit; it is satisfied by an enumeration of each cubic graph's neighbours.

theorem Complexity.Frontier.LocalLayout.cutSize_improve_cubic_le {V : Type u_1} {E : Type u_2} [Fintype E] (G : Multigraph V E) (I : Finset V) (hI : ∀ (e : E), ¬(G.src e ∈ I ∧ G.tgt e ∈ I)) (edges : (v : V) → Fin 3 ≃ ↑(G.edgesAt v)) (key : V → ℝ) (t : ℝ) : (G.cutSize fun (v : V) => decide (improve I (fun (v : V) (i : Fin 3) => G.otherEnd v ↑((edges v) i)) key v < t)) ≤ G.cutSize fun (v : V) => decide (key v < t)

A cubic multigraph can use its actual incident-edge enumerations, with no additional assumption about boundary states or the distribution of keys.