Ordering a cubic graph by median edge scores

Give every edge of a cubic graph a real score. Each vertex has three incident edges, hence a median score, and we list the vertices by their medians. This file bounds the cut of every prefix of that list in terms of 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.

The cut of a prefix (card_crossingFinset_le). Let P be a set of vertices whose medians are all at most some m, while the medians outside P are all at least m. An edge leaving P that scores below a threshold t ≤ m is charged to its endpoint outside P: that endpoint has its median above the edge's score, so it is charged at most once. An edge scoring at least a threshold t' > m is charged to its endpoint inside P, again at most once. If a + i δ ≤ m < a + (i + 1) δ, every vertex charged in this way straddles a + i δ or is an endpoint of an edge scoring in the window [a + i δ, a + (i + 1) δ), so the cut has at most

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

edges. If m lies below the grid, or above it, the cut is at most three times the number of edges in the lower, or upper, tail.

The layout (exists_key_of_edgeScore). Listing the vertices by median, with ties broken arbitrarily, every prefix has the property above, so all prefix cuts are bounded at once.

def Complexity.Frontier.EdgeStraddles {W : Type} [Fintype W] (H : SimpleGraph W) [DecidableRel H.Adj] (score : Sym2 W → ℝ) (t : ℝ) (v : W) : Prop

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

Equations

• Complexity.Frontier.EdgeStraddles H score t v = ∃ e ∈ H.incidenceFinset v, score e < t ∧ ∃ e' ∈ H.incidenceFinset v, t ≤ score e'

@[instance_reducible]

noncomputable instance Complexity.Frontier.instDecidablePredEdgeStraddles {W : Type} [Fintype W] (H : SimpleGraph W) [DecidableRel H.Adj] (score : Sym2 W → ℝ) (t : ℝ) : DecidablePred (EdgeStraddles H score t)

Equations

• Complexity.Frontier.instDecidablePredEdgeStraddles H score t x✝ = id inferInstance

def Complexity.Frontier.IsMedian {W : Type} [Fintype W] (H : SimpleGraph W) [DecidableRel H.Adj] (score : Sym2 W → ℝ) (v : W) (m : ℝ) : Prop

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

Equations

• Complexity.Frontier.IsMedian H score v m = (2 ≤ {e ∈ H.incidenceFinset v | score e ≤ m}.card ∧ 2 ≤ {e ∈ H.incidenceFinset v | m ≤ score e}.card)

theorem Complexity.Frontier.card_incidenceFinset_of_regular {W : Type} [Fintype W] {H : SimpleGraph W} [DecidableRel H.Adj] (regular : H.IsRegularOfDegree 3) (v : W) : (H.incidenceFinset v).card = 3

theorem Complexity.Frontier.exists_isMedian {W : Type} [Fintype W] {H : SimpleGraph W} [DecidableRel H.Adj] (regular : H.IsRegularOfDegree 3) (score : Sym2 W → ℝ) (v : W) : ∃ (m : ℝ), IsMedian H score v m

Every vertex of a cubic graph has a median edge score.

theorem Complexity.Frontier.IsMedian.card_lt_le_one {W : Type} [Fintype W] {H : SimpleGraph W} [DecidableRel H.Adj] (regular : H.IsRegularOfDegree 3) {score : Sym2 W → ℝ} {v : W} {m : ℝ} (h : IsMedian H score v m) : {e ∈ H.incidenceFinset v | m < score e}.card ≤ 1

At most one edge at a vertex scores above a median.

theorem Complexity.Frontier.IsMedian.card_gt_le_one {W : Type} [Fintype W] {H : SimpleGraph W} [DecidableRel H.Adj] (regular : H.IsRegularOfDegree 3) {score : Sym2 W → ℝ} {v : W} {m : ℝ} (h : IsMedian H score v m) : {e ∈ H.incidenceFinset v | score e < m}.card ≤ 1

At most one edge at a vertex scores below a median.

theorem Complexity.Frontier.card_le_of_endpoints {W : Type} {C : Finset (Sym2 W)} {Q : Finset W} (hend : ∀ e ∈ C, ∃ v ∈ Q, v ∈ e) (huniq : ∀ v ∈ Q, ∀ e ∈ C, ∀ e' ∈ C, v ∈ e → v ∈ e' → e = e') : C.card ≤ Q.card

Edges each with an endpoint in Q, no two sharing such an endpoint, number at most |Q|.

theorem Complexity.Frontier.card_endpoints_le {W : Type} [Fintype W] [DecidableEq W] (D : Finset (Sym2 W)) : {w : W | ∃ e ∈ D, w ∈ e}.card ≤ 2 * D.card

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

The cut of a prefix

theorem Complexity.Frontier.card_cut_lt_le {W : Type} [Fintype W] {H : SimpleGraph W} [DecidableRel H.Adj] {score : Sym2 W → ℝ} {med : W → ℝ} {P : Finset W} {m : ℝ} [DecidableEq W] (regular : H.IsRegularOfDegree 3) (hmed : ∀ (v : W), IsMedian H score v (med v)) (hPc : ∀ v ∉ P, m ≤ med v) {t : ℝ} (ht : t ≤ m) : {e ∈ H.crossingFinset P | score e < t}.card ≤ {v : W | v ∉ P ∧ ∃ e ∈ H.incidenceFinset v, score e < t}.card

Edges leaving P that score below a threshold t ≤ m are no more than the vertices outside P with an edge scoring below t.

theorem Complexity.Frontier.card_cut_ge_le {W : Type} [Fintype W] {H : SimpleGraph W} [DecidableRel H.Adj] {score : Sym2 W → ℝ} {med : W → ℝ} {P : Finset W} {m : ℝ} [DecidableEq W] (regular : H.IsRegularOfDegree 3) (hmed : ∀ (v : W), IsMedian H score v (med v)) (hP : ∀ u ∈ P, med u ≤ m) {t : ℝ} (ht : m < t) : {e ∈ H.crossingFinset P | t ≤ score e}.card ≤ {u : W | u ∈ P ∧ ∃ e ∈ H.incidenceFinset u, t ≤ score e}.card

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 Complexity.Frontier.card_crossingFinset_le {W : Type} [Fintype W] {H : SimpleGraph W} [DecidableRel H.Adj] {score : Sym2 W → ℝ} {med : W → ℝ} {P : Finset W} {m : ℝ} (regular : H.IsRegularOfDegree 3) (hmed : ∀ (v : W), IsMedian H score v (med v)) (hP : ∀ u ∈ P, med u ≤ m) (hPc : ∀ v ∉ P, m ≤ med v) {a δ : ℝ} (hδ : 0 < δ) (M : ℕ) {B : ℝ} (low : 3 * ↑{e ∈ H.edgeFinset | score e < a}.card ≤ B) (high : 3 * ↑{e ∈ H.edgeFinset | a + ↑M * δ ≤ score e}.card ≤ B) (mid : ∀ i < M, ↑{v : W | EdgeStraddles H score (a + ↑i * δ) v}.card + 3 * ↑{e ∈ H.edgeFinset | a + ↑i * δ ≤ score e ∧ score e < a + (↑i + 1) * δ}.card ≤ B) : ↑(H.crossingFinset P).card ≤ B

The cut of a prefix. Let P have all medians at most m and all medians outside it at least m. If the edges in each tail, and the straddling vertices and window edges at every grid threshold, are few, then few edges leave P.

The layout

theorem Complexity.Frontier.exists_key_of_edgeScore {W : Type} [Fintype W] {H : SimpleGraph W} [DecidableRel H.Adj] (regular : H.IsRegularOfDegree 3) (score : Sym2 W → ℝ) {a δ : ℝ} (hδ : 0 < δ) (M : ℕ) {B : ℝ} (low : 3 * ↑{e ∈ H.edgeFinset | score e < a}.card ≤ B) (high : 3 * ↑{e ∈ H.edgeFinset | a + ↑M * δ ≤ score e}.card ≤ B) (mid : ∀ i < M, ↑{v : W | EdgeStraddles H score (a + ↑i * δ) v}.card + 3 * ↑{e ∈ H.edgeFinset | a + ↑i * δ ≤ score e ∧ score e < a + (↑i + 1) * δ}.card ≤ B) : ∃ (key : W → ℕ), Function.Injective key ∧ ∀ (t : ℕ), ↑(H.crossingFinset {w : W | key w < t}).card ≤ B

The median layout. Score the edges of a cubic graph and fix a grid a, a + δ, ..., a + M δ. If three times the edges 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 median score gives a layout all of whose prefixes are crossed by at most B edges.