Jumping the median band of edge scores

Fix c > 0 and a real score on the edges of a cubic graph. An edge is low when its score is below -c, in the band when its score lies in [-c, c), and high when its score is at least c. Label the band edges by blocks so that band edges sharing a vertex share a label, for example by the connected components of the band.

The band-jump order lists the low edges by score, then the band blocks one whole block at a time, then the high edges by score. The blocks are taken in increasing order of the imbalance B_j - A_j, where A_j (resp. B_j) counts the vertices touching block j with a low (resp. high) edge. Between blocks, a bag holds the vertices with no band edge but both a low and a high edge, the high endpoints of the finished blocks, and the low endpoints of the blocks still to come. The vertices straddling -c are those of the first kind together with all A_j vertices, and those straddling c are those of the first kind together with all B_j vertices. Taking the blocks by increasing imbalance keeps every prefix sum of the imbalances at most max 0 (∑ (B_j - A_j)), so every bag of the band phase has at most the larger of the two straddling counts plus the vertices of the block in progress.

• exists_pathDecomposition_of_bandJump: if every threshold t < -c or t ≥ c has at most B vertices with an edge scoring at most t and one scoring at least t, and for every block j both straddling counts of ±c plus the endpoints of block j are at most B, then every bag has at most B vertices.
• card_filter_edgeScore_le_window: a threshold t ∈ [u, u') has at most the straddling vertices of u plus twice the edges scoring in [u, u').
• card_filter_edgeScore_le_of_grid: grid thresholds a + i δ with few straddling vertices and few edges in each window bound every t ∈ [a, a + M δ).
• card_filter_edgeScore_le_of_grids: a low grid reaching -c, a high grid starting at or below c, and the two tails bound every threshold outside the band, as required by exists_pathDecomposition_of_bandJump.

theorem Algebraic.Cutwidth.Gaussian.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

A threshold t ∈ [u, u'): every 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.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

Threshold grid. If every threshold a + i δ, i < M, has its straddling vertices plus twice the edges scoring in [a + i δ, a + (i + 1) δ) at most B, then every t ∈ [a, a + M δ) has at most B vertices with an edge scoring at most t and an edge scoring at least t.

theorem Algebraic.Cutwidth.Gaussian.card_filter_edgeScore_le_of_grids {W : Type} [Fintype W] [DecidableEq W] (H : SimpleGraph W) [DecidableRel H.Adj] (score : Sym2 W → ℝ) {c a₁ δ₁ a₂ δ₂ B : ℝ} (hδ₁ : 0 < δ₁) (hδ₂ : 0 < δ₂) (M₁ M₂ : ℕ) (hlow : -c ≤ a₁ + ↑M₁ * δ₁) (hhigh : a₂ ≤ c) (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) (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 : ℝ) (ht : t < -c ∨ c ≤ t) : ↑{v : W | (∃ e ∈ H.edgeFinset, v ∈ e ∧ score e ≤ t) ∧ ∃ e ∈ H.edgeFinset, v ∈ e ∧ t ≤ score e}.card ≤ B

Thresholds outside the band. Take a low grid a₁ + i δ₁, i ≤ M₁, reaching -c and a high grid a₂ + i δ₂, i ≤ M₂, starting at or below c. If twice the edges scoring below a₁, twice the edges scoring at least a₂ + M₂ δ₂, and the grid counts of both grids are at most B, then every threshold t < -c or t ≥ c has at most B vertices with an edge scoring at most t and an edge scoring at least t.

theorem Algebraic.Cutwidth.Gaussian.exists_pathDecomposition_of_bandJump {W : Type} [Fintype W] [DecidableEq W] (H : SimpleGraph W) [DecidableRel H.Adj] (regular : H.IsRegularOfDegree 3) (score : Sym2 W → ℝ) {c : ℝ} (hc : 0 < c) (block : Sym2 W → ℕ) (hblock : ∀ (v : W), ∀ e ∈ H.incidenceFinset v, ∀ e' ∈ H.incidenceFinset v, -c ≤ score e → score e < c → -c ≤ score e' → score e' < c → block e = block e') {B : ℝ} (outside : ∀ (t : ℝ), t < -c ∨ c ≤ t → ↑{v : W | (∃ e ∈ H.edgeFinset, v ∈ e ∧ score e ≤ t) ∧ ∃ e ∈ H.edgeFinset, v ∈ e ∧ t ≤ score e}.card ≤ B) (inside : ∀ (j : ℕ), ↑{v : W | EdgeStraddles H score (-c) v}.card + ↑{v : W | ∃ e ∈ H.edgeFinset, v ∈ e ∧ -c ≤ score e ∧ score e < c ∧ block e = j}.card ≤ B ∧ ↑{v : W | EdgeStraddles H score c v}.card + ↑{v : W | ∃ e ∈ H.edgeFinset, v ∈ e ∧ -c ≤ score e ∧ score e < c ∧ block e = j}.card ≤ B) : ∃ (D : PathDecomposition H), ∀ (k : Fin D.length), ↑(D.bag k).card ≤ B

Band-jump path decomposition. Let c > 0 and label the band edges -c ≤ score e < c so that band edges sharing a vertex share a label. Suppose every threshold t < -c or t ≥ c has at most B vertices with an edge scoring at most t and an edge scoring at least t, and for every label j the vertices straddling -c, as well as those straddling c, together with the endpoints of the band edges labelled j, number at most B. Then some path decomposition has every bag of at most B vertices.