Path decompositions from edge scores: proofs

A cubic vertex has three incident edges. If a threshold has incident edges on both sides, one side holds one edge and the other two, so four ordered pairs of distinct incident edges are separated by the threshold.

For the decomposition, list the edges in nondecreasing score order and let bag k hold the vertices with an incident edge at a position at most k and another at a position at least k. With t the score of the k-th edge, every vertex of bag k has an edge scoring at most t and an edge scoring at least t. If t lies below the grid or above it, the vertex is an endpoint of a tail edge. Otherwise a + i δ ≤ t < a + (i + 1) δ for some i < M, and the vertex straddles a + i δ or is an endpoint of an edge in the window [a + i δ, a + (i + 1) δ).

theorem Algebraic.Cutwidth.Gaussian.Internal.four_le_between_pairs {t p q r : ℝ} (hlt : p < t ∨ q < t ∨ r < t) (hge : t ≤ p ∨ t ≤ q ∨ t ≤ r) : 4 ≤ ((if Between t p q then 1 else 0) + if Between t p r then 1 else 0) + (((if Between t q p then 1 else 0) + if Between t q r then 1 else 0) + ((if Between t r p then 1 else 0) + if Between t r q then 1 else 0))

Three reals on both sides of a threshold give four ordered separated pairs.

theorem Algebraic.Cutwidth.Gaussian.Internal.indicator_edgeStraddles_le {W : Type} [Fintype W] [DecidableEq W] (H : SimpleGraph W) [DecidableRel H.Adj] (regular : H.IsRegularOfDegree 3) (score : Sym2 W → ℝ) (t : ℝ) (v : W) : (if EdgeStraddles H score t v then 1 else 0) ≤ 1 / 4 * ∑ e ∈ H.incidenceFinset v, ∑ e' ∈ (H.incidenceFinset v).erase e, if Between t (score e) (score e') then 1 else 0

In a cubic graph, a straddling vertex has at least four ordered pairs of incident edges separated by the threshold.

theorem Algebraic.Cutwidth.Gaussian.Internal.mem_incidenceFinset_iff {W : Type} [Fintype W] [DecidableEq W] (H : SimpleGraph W) [DecidableRel H.Adj] {v : W} {e : Sym2 W} : e ∈ H.incidenceFinset v ↔ e ∈ H.edgeFinset ∧ v ∈ e

The edges at v are the edges of the graph containing v.

theorem Algebraic.Cutwidth.Gaussian.Internal.card_filter_exists_mem_le {W : Type} [Fintype W] [DecidableEq W] (F : Finset (Sym2 W)) : {v : W | ∃ e ∈ F, v ∈ e}.card ≤ 2 * F.card

A set of edges has at most two endpoints per edge.

theorem Algebraic.Cutwidth.Gaussian.Internal.card_filter_edgeScore_le_of_lt {W : Type} [Fintype W] [DecidableEq W] (H : SimpleGraph W) [DecidableRel H.Adj] (score : Sym2 W → ℝ) {a t : ℝ} (ht : t < a) : ↑{v : W | (∃ e ∈ H.edgeFinset, v ∈ e ∧ score e ≤ t) ∧ ∃ e ∈ H.edgeFinset, v ∈ e ∧ t ≤ score e}.card ≤ 2 * ↑{e ∈ H.edgeFinset | score e < a}.card

Below a: a vertex with an edge scoring at most t < a is an endpoint of an edge scoring below a.

theorem Algebraic.Cutwidth.Gaussian.Internal.card_filter_edgeScore_le_of_ge {W : Type} [Fintype W] [DecidableEq W] (H : SimpleGraph W) [DecidableRel H.Adj] (score : Sym2 W → ℝ) {b t : ℝ} (ht : b ≤ t) : ↑{v : W | (∃ e ∈ H.edgeFinset, v ∈ e ∧ score e ≤ t) ∧ ∃ e ∈ H.edgeFinset, v ∈ e ∧ t ≤ score e}.card ≤ 2 * ↑{e ∈ H.edgeFinset | b ≤ score e}.card

At or above b: a vertex with an edge scoring at least t ≥ b is an endpoint of an edge scoring at least b.

theorem Algebraic.Cutwidth.Gaussian.Internal.card_filter_edgeScore_le_window {W : Type} [Fintype W] [DecidableEq W] (H : SimpleGraph W) [DecidableRel H.Adj] (score : Sym2 W → ℝ) {u t u' : ℝ} (hu : u ≤ t) (hu' : t < u') : ↑{v : W | (∃ e ∈ H.edgeFinset, v ∈ e ∧ score e ≤ t) ∧ ∃ e ∈ H.edgeFinset, v ∈ e ∧ t ≤ score e}.card ≤ ↑{v : W | EdgeStraddles H score u v}.card + 2 * ↑{e ∈ H.edgeFinset | u ≤ score e ∧ score e < u'}.card

In a window u ≤ t < u': a vertex with an edge scoring at most t and an edge scoring at least t straddles u or is an endpoint of an edge scoring in [u, u').

theorem Algebraic.Cutwidth.Gaussian.Internal.card_filter_edgeScore_le_of_grid {W : Type} [Fintype W] [DecidableEq W] (H : SimpleGraph W) [DecidableRel H.Adj] (score : Sym2 W → ℝ) {a δ : ℝ} (hδ : 0 < δ) (M : ℕ) {B : ℝ} (mid : ∀ i < M, ↑{v : W | EdgeStraddles H score (a + ↑i * δ) v}.card + 2 * ↑{e ∈ H.edgeFinset | a + ↑i * δ ≤ score e ∧ score e < a + (↑i + 1) * δ}.card ≤ B) {t : ℝ} (ha : a ≤ t) (ht : t < a + ↑M * δ) : ↑{v : W | (∃ e ∈ H.edgeFinset, v ∈ e ∧ score e ≤ t) ∧ ∃ e ∈ H.edgeFinset, v ∈ e ∧ t ≤ score e}.card ≤ B

Inside a grid a + i δ, i ≤ M: if every threshold has few straddling vertices and few edges in the following window, then so does every t ∈ [a, a + M δ).

theorem Algebraic.Cutwidth.Gaussian.Internal.card_filter_edgeScore_le {W : Type} [Fintype W] [DecidableEq W] (H : SimpleGraph W) [DecidableRel H.Adj] (score : Sym2 W → ℝ) {a δ : ℝ} (hδ : 0 < δ) (M : ℕ) {B : ℝ} (low : 2 * ↑{e ∈ H.edgeFinset | score e < a}.card ≤ B) (high : 2 * ↑{e ∈ H.edgeFinset | a + ↑M * δ ≤ score e}.card ≤ B) (mid : ∀ i < M, ↑{v : W | EdgeStraddles H score (a + ↑i * δ) v}.card + 2 * ↑{e ∈ H.edgeFinset | a + ↑i * δ ≤ score e ∧ score e < a + (↑i + 1) * δ}.card ≤ B) (t : ℝ) : ↑{v : W | (∃ e ∈ H.edgeFinset, v ∈ e ∧ score e ≤ t) ∧ ∃ e ∈ H.edgeFinset, v ∈ e ∧ t ≤ score e}.card ≤ B

Every vertex with an edge scoring at most t and an edge scoring at least t is counted by a tail or by one threshold of the grid.

theorem Algebraic.Cutwidth.Gaussian.Internal.exists_pathDecomposition_subset_edgeScore {W : Type} [Fintype W] [DecidableEq W] (H : SimpleGraph W) [DecidableRel H.Adj] (regular : H.IsRegularOfDegree 3) (score : Sym2 W → ℝ) : ∃ (D : PathDecomposition H), ∀ (k : Fin D.length), ∃ (t : ℝ), D.bag k ⊆ {v : W | (∃ e ∈ H.edgeFinset, v ∈ e ∧ score e ≤ t) ∧ ∃ e ∈ H.edgeFinset, v ∈ e ∧ t ≤ score e}

Score-order path decomposition. List the edges of a cubic graph in nondecreasing score order and let bag k hold the vertices with an incident edge at a position at most k and another at a position at least k. Each bag lies inside the vertices with an edge scoring at most t and an edge scoring at least t, where t is the score of the k-th edge.

theorem Algebraic.Cutwidth.Gaussian.Internal.exists_pathDecomposition_of_edgeScore {W : Type} [Fintype W] [DecidableEq W] (H : SimpleGraph W) [DecidableRel H.Adj] (regular : H.IsRegularOfDegree 3) (score : Sym2 W → ℝ) {a δ : ℝ} (hδ : 0 < δ) (M : ℕ) {B : ℝ} (low : 2 * ↑{e ∈ H.edgeFinset | score e < a}.card ≤ B) (high : 2 * ↑{e ∈ H.edgeFinset | a + ↑M * δ ≤ score e}.card ≤ B) (mid : ∀ i < M, ↑{v : W | EdgeStraddles H score (a + ↑i * δ) v}.card + 2 * ↑{e ∈ H.edgeFinset | a + ↑i * δ ≤ score e ∧ score e < a + (↑i + 1) * δ}.card ≤ B) : ∃ (D : PathDecomposition H), ∀ (k : Fin D.length), ↑(D.bag k).card ≤ B

Edge-score path decomposition. Listing the edges of a cubic graph by score, bag k holds the vertices with edges at positions on both sides of k. Every bag has at most B vertices.