Ordering a cubic multigraph by median edge scores

Give every edge of a multigraph a real score, and let every vertex have exactly three edges. Each vertex then has a median score (Multigraph.exists_isMedian, from median3), and listing the vertices by their medians is a layout. This file bounds the frontiers of that layout by how the scores fall around a grid of thresholds a, a + δ, ..., a + M δ. A vertex straddles a threshold t when one of its edges scores below t and another at least t (Multigraph.EdgeStraddles).

The cut of a prefix (Multigraph.ncard_edgeCut_le_of_isMedian). Let P be a set of vertices whose medians are at most some m, while the medians outside P are at least m.

• An edge leaving P that scores below a threshold t ≤ m is charged to its endpoint outside P. That endpoint straddles t, and it is charged at most once, since at most one of its three edges scores below its median.
• An edge leaving P that scores at least a threshold t' > m is charged to its endpoint inside P, again at most once. That endpoint has an edge scoring at most its median ≤ m: if this edge scores below t, the endpoint straddles t; otherwise the edge scores in the window [t, t').

So if a + i δ ≤ m < a + (i + 1) δ, the cut of P has at most

#(vertices straddling a + i δ) + 3 #(edges scoring in the window [a + i δ, a + (i + 1) δ))

edges. If m lies below the grid, or above it, the cut has at most three times as many edges as score in the lower tail, or in the upper tail.

The layout (Multigraph.exists_width_le_of_edgeScore). Every prefix of the layout by medians has the property above, so a single bound on the tails, the straddling vertices and the windows bounds the width.

Main definitions

• Cslib.Circuits.Frontier.Multigraph.EdgeStraddles: a vertex straddles a threshold.
• Cslib.Circuits.Frontier.Multigraph.IsMedian: a median of the scores of the edges at a vertex.

Main results

• Cslib.Circuits.Frontier.Multigraph.exists_isMedian: medians exist at vertices with three edges.
• Cslib.Circuits.Frontier.Multigraph.ncard_edgeCut_le_of_isMedian: the cut of a prefix.
• Cslib.Circuits.Frontier.Multigraph.exists_width_le_of_edgeScore: the layout by median scores.

def Cslib.Circuits.Frontier.Multigraph.EdgeStraddles {V : Type u_1} {E : Type u_2} (G : Multigraph V E) {α : Type u_3} [LinearOrder α] (score : E → α) (t : α) (v : V) : Prop

The vertex v straddles the threshold t under the edge scores score: an edge at v scores below t and another scores at least t.

def Cslib.Circuits.Frontier.Multigraph.IsMedian {V : Type u_1} {E : Type u_2} (G : Multigraph V E) {α : Type u_3} [LinearOrder α] (score : E → α) (v : V) (m : α) : Prop

m is a median of the scores of the edges at v: at least two edges at v score at most m, and at least two score at least m.

theorem Cslib.Circuits.Frontier.Multigraph.edgeStraddles_congr {V : Type u_1} {E : Type u_2} {G : Multigraph V E} {α : Type u_3} [LinearOrder α] {score score' : E → α} {t : α} {v : V} (h : ∀ e ∈ G.incidenceSet v, score e = score' e) : G.EdgeStraddles score t v ↔ G.EdgeStraddles score' t v

Whether v straddles t depends only on the scores of the edges at v.

theorem Cslib.Circuits.Frontier.Multigraph.exists_isMedian {V : Type u_1} {E : Type u_2} {G : Multigraph V E} {α : Type u_3} [LinearOrder α] {v : V} (hv : (G.incidenceSet v).ncard = 3) (score : E → α) : ∃ (m : α), G.IsMedian score v m

Medians exist. At a vertex with three edges, the median of their three scores is a median.

theorem Cslib.Circuits.Frontier.Multigraph.IsMedian.exists_score_le {V : Type u_1} {E : Type u_2} {G : Multigraph V E} {α : Type u_3} [LinearOrder α] {score : E → α} {v : V} {m : α} (h : G.IsMedian score v m) : ∃ e ∈ G.incidenceSet v, score e ≤ m

Some edge at v scores at most a median.

theorem Cslib.Circuits.Frontier.Multigraph.IsMedian.exists_le_score {V : Type u_1} {E : Type u_2} {G : Multigraph V E} {α : Type u_3} [LinearOrder α] {score : E → α} {v : V} {m : α} (h : G.IsMedian score v m) : ∃ e ∈ G.incidenceSet v, m ≤ score e

Some edge at v scores at least a median.

theorem Cslib.Circuits.Frontier.Multigraph.IsMedian.eq_of_score_lt {V : Type u_1} {E : Type u_2} {G : Multigraph V E} {α : Type u_3} [LinearOrder α] {score : E → α} {v : V} {m : α} [Finite E] (h : G.IsMedian score v m) (hv : (G.incidenceSet v).ncard = 3) {e e' : E} (he : e ∈ G.incidenceSet v) (he' : e' ∈ G.incidenceSet v) (hlt : score e < m) (hlt' : score e' < m) : e = e'

At a vertex with three edges, at most one edge scores below a median.

theorem Cslib.Circuits.Frontier.Multigraph.IsMedian.eq_of_lt_score {V : Type u_1} {E : Type u_2} {G : Multigraph V E} {α : Type u_3} [LinearOrder α] {score : E → α} {v : V} {m : α} [Finite E] (h : G.IsMedian score v m) (hv : (G.incidenceSet v).ncard = 3) {e e' : E} (he : e ∈ G.incidenceSet v) (he' : e' ∈ G.incidenceSet v) (hlt : m < score e) (hlt' : m < score e') : e = e'

At a vertex with three edges, at most one edge scores above a median.

The cut of a prefix

theorem Cslib.Circuits.Frontier.Multigraph.ncard_edgeCut_score_lt_le {V : Type u_1} {E : Type u_2} {G : Multigraph V E} {α : Type u_3} [LinearOrder α] [Finite E] {score : E → α} {med : V → α} {P : Set V} {m : α} [Finite V] (h3 : ∀ (v : V), (G.incidenceSet v).ncard = 3) (hmed : ∀ (v : V), G.IsMedian score v (med v)) (hPc : ∀ v ∉ P, m ≤ med v) {t : α} (ht : t ≤ m) : {e : E | e ∈ G.edgeCut P ∧ score e < t}.ncard ≤ {v : V | v ∉ P ∧ G.EdgeStraddles score t v}.ncard

Charging low edges. If the medians outside P are at least m, the edges leaving P that score below a threshold t ≤ m are no more than the vertices outside P that straddle t.

theorem Cslib.Circuits.Frontier.Multigraph.ncard_edgeCut_le_score_le {V : Type u_1} {E : Type u_2} {G : Multigraph V E} {α : Type u_3} [LinearOrder α] [Finite E] {score : E → α} {med : V → α} {P : Set V} {m : α} [Finite V] (h3 : ∀ (v : V), (G.incidenceSet v).ncard = 3) (hmed : ∀ (v : V), G.IsMedian score v (med v)) (hP : ∀ u ∈ P, med u ≤ m) {t : α} (ht : m < t) : {e : E | e ∈ G.edgeCut P ∧ t ≤ score e}.ncard ≤ {u : V | u ∈ P ∧ ∃ e ∈ G.incidenceSet u, t ≤ score e}.ncard

Charging high edges. If the medians inside P are at most m, the edges leaving P that score at least a threshold t > m are no more than the vertices inside P with an edge scoring at least t.

theorem Cslib.Circuits.Frontier.Multigraph.ncard_endpoints_le {V : Type u_1} {E : Type u_2} {G : Multigraph V E} [Finite E] (F : Set E) : {w : V | ∃ e ∈ F, G.src e = w ∨ G.tgt e = w}.ncard ≤ 2 * F.ncard

The endpoints of a set of edges number at most twice the edges.

theorem Cslib.Circuits.Frontier.Multigraph.ncard_edgeCut_le_of_isMedian {V : Type u_1} {E : Type u_2} {G : Multigraph V E} [Finite E] [Finite V] (h3 : ∀ (v : V), (G.incidenceSet v).ncard = 3) {score : E → ℝ} {med : V → ℝ} (hmed : ∀ (v : V), G.IsMedian score v (med v)) {P : Set V} {m : ℝ} (hP : ∀ u ∈ P, med u ≤ m) (hPc : ∀ v ∉ P, m ≤ med v) {a δ : ℝ} (hδ : 0 < δ) {M : ℕ} {B : ℝ} (low : 3 * ↑{e : E | score e < a}.ncard ≤ B) (high : 3 * ↑{e : E | a + ↑M * δ ≤ score e}.ncard ≤ B) (mid : ∀ i < M, ↑{v : V | G.EdgeStraddles score (a + ↑i * δ) v}.ncard + 3 * ↑{e : E | a + ↑i * δ ≤ score e ∧ score e < a + (↑i + 1) * δ}.ncard ≤ B) : ↑(G.edgeCut P).ncard ≤ B

The cut of a prefix. Let the vertices of P have medians at most m, and the others medians at least m. If three times the edges scoring in each tail, and the vertices straddling each grid threshold plus three times the edges scoring in the following window, are at most B, then at most B edges leave P.

The layout

theorem Cslib.Circuits.Frontier.Multigraph.exists_width_le_of_edgeScore {V : Type u_1} {E : Type u_2} {G : Multigraph V E} [Finite V] [Finite E] (h3 : ∀ (v : V), (G.incidenceSet v).ncard = 3) (score : E → ℝ) {a δ : ℝ} (hδ : 0 < δ) (M : ℕ) {B : ℝ} (low : 3 * ↑{e : E | score e < a}.ncard ≤ B) (high : 3 * ↑{e : E | a + ↑M * δ ≤ score e}.ncard ≤ B) (mid : ∀ i < M, ↑{v : V | G.EdgeStraddles score (a + ↑i * δ) v}.ncard + 3 * ↑{e : E | a + ↑i * δ ≤ score e ∧ score e < a + (↑i + 1) * δ}.ncard ≤ B) : ∃ (π : Layout V), ↑(G.width π) ≤ B

The layout by median scores. Let every vertex have three edges, score the edges, and fix a grid a, a + δ, ..., a + M δ. If three times the edges scoring in each tail, and the vertices straddling each grid threshold plus three times the edges scoring in the following window, are at most B, then listing the vertices by the medians of their scores gives a layout of width at most B.