Jumping the median band of edge scores: proofs

Fix c > 0. An edge is low when its score is below -c, in the band when its score lies in [-c, c), and high otherwise. The band edges carry block labels, and band edges sharing a vertex carry the same label. Block j has A_j vertices touching it with a low edge and B_j vertices touching it with a high edge.

The band-jump score keeps the low and high scores and gives every band edge of block j the same value blockValue j ∈ (-c, c). These values are distinct on the labels in use and increase with the imbalance B_j - A_j, ties broken by label. The score-order decomposition of this score has each bag inside the vertices with a jumped score at most t and one at least t, for some t.

• For t < -c or t ≥ c, these vertices also have a score at most t and one at least t.
• For -c ≤ t < c, every such vertex either has no band edge but a low and a high edge, or touches a block valued below t and has a high edge, or touches a block valued above t and has a low edge, or touches the block valued t. The blocks valued below t all have imbalance at most that of every other block, so sum_add_sum_sdiff_le_max bounds the middle two counts by max (∑ A_j) (∑ B_j). The vertices straddling -c contain the first kind and all A_j vertices disjointly, and those straddling c contain the first kind and all B_j vertices disjointly.

Exchanging a prefix

theorem Algebraic.Cutwidth.Gaussian.Internal.sum_add_sum_sdiff_le_max {ι : Type u_1} [DecidableEq ι] {L F : Finset ι} (hF : F ⊆ L) (a b : ι → ℕ) (hab : ∀ i ∈ F, ∀ j ∈ L \ F, ↑(b i) - ↑(a i) ≤ ↑(b j) - ↑(a j)) : ∑ i ∈ F, b i + ∑ j ∈ L \ F, a j ≤ max (∑ i ∈ L, a i) (∑ i ∈ L, b i)

Prefix exchange. If every imbalance b i - a i on F ⊆ L is at most every imbalance on L \ F, then counting b on F and a on L \ F gives at most the larger total.

Ranks by a key

def Algebraic.Cutwidth.Gaussian.Internal.keyRank {ι : Type u_1} {α : Type u_2} [LinearOrder α] (L : Finset ι) (κ : ι → α) (j : ι) : ℕ

The number of elements of L whose key is below the key of j.

Equations

• Algebraic.Cutwidth.Gaussian.Internal.keyRank L κ j = {i ∈ L | κ i < κ j}.card

theorem Algebraic.Cutwidth.Gaussian.Internal.keyRank_le_card {ι : Type u_1} {α : Type u_2} [LinearOrder α] (L : Finset ι) (κ : ι → α) (j : ι) : keyRank L κ j ≤ L.card

theorem Algebraic.Cutwidth.Gaussian.Internal.keyRank_le_keyRank {ι : Type u_1} {α : Type u_2} [LinearOrder α] (L : Finset ι) (κ : ι → α) {i j : ι} (h : κ i ≤ κ j) : keyRank L κ i ≤ keyRank L κ j

theorem Algebraic.Cutwidth.Gaussian.Internal.keyRank_lt_keyRank {ι : Type u_1} {α : Type u_2} [LinearOrder α] (L : Finset ι) (κ : ι → α) {i j : ι} (hi : i ∈ L) (h : κ i < κ j) : keyRank L κ i < keyRank L κ j

theorem Algebraic.Cutwidth.Gaussian.Internal.lt_of_keyRank_lt {ι : Type u_1} {α : Type u_2} [LinearOrder α] (L : Finset ι) (κ : ι → α) {i j : ι} (h : keyRank L κ i < keyRank L κ j) : κ i < κ j

theorem Algebraic.Cutwidth.Gaussian.Internal.eq_of_keyRank_eq {ι : Type u_1} {α : Type u_2} [LinearOrder α] (L : Finset ι) (κ : ι → α) (hκ : Function.Injective κ) {i j : ι} (hi : i ∈ L) (hj : j ∈ L) (h : keyRank L κ i = keyRank L κ j) : i = j

Blocks of band edges

noncomputable def Algebraic.Cutwidth.Gaussian.Internal.scoreSpan {W : Type} [Fintype W] [DecidableEq W] (H : SimpleGraph W) [DecidableRel H.Adj] (score : Sym2 W → ℝ) (t : ℝ) : Finset W

The vertices with an edge scoring at most t and an edge scoring at least t.

Equations

• Algebraic.Cutwidth.Gaussian.Internal.scoreSpan H score t = {v : W | (∃ e ∈ H.edgeFinset, v ∈ e ∧ score e ≤ t) ∧ ∃ e ∈ H.edgeFinset, v ∈ e ∧ t ≤ score e}

def Algebraic.Cutwidth.Gaussian.Internal.BandBlocks {W : Type} [Fintype W] (H : SimpleGraph W) [DecidableRel H.Adj] (score : Sym2 W → ℝ) (c : ℝ) (block : Sym2 W → ℕ) : Prop

Band edges -c ≤ score e < c sharing a vertex carry the same block label.

Equations

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

noncomputable def Algebraic.Cutwidth.Gaussian.Internal.bandLabels {W : Type} [Fintype W] (H : SimpleGraph W) [DecidableRel H.Adj] (score : Sym2 W → ℝ) (c : ℝ) (block : Sym2 W → ℕ) : Finset ℕ

The block labels of the band edges.

Equations

• Algebraic.Cutwidth.Gaussian.Internal.bandLabels H score c block = Finset.image block ({e ∈ H.edgeFinset | -c ≤ score e ∧ score e < c})

noncomputable def Algebraic.Cutwidth.Gaussian.Internal.bandFree {W : Type} [Fintype W] [DecidableEq W] (H : SimpleGraph W) [DecidableRel H.Adj] (score : Sym2 W → ℝ) (c : ℝ) : Finset W

The vertices without a band edge but with an edge scoring below -c and an edge scoring at least c.

Equations

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

noncomputable def Algebraic.Cutwidth.Gaussian.Internal.blockVertices {W : Type} [Fintype W] [DecidableEq W] (H : SimpleGraph W) [DecidableRel H.Adj] (score : Sym2 W → ℝ) (c : ℝ) (block : Sym2 W → ℕ) (j : ℕ) : Finset W

The endpoints of the band edges of block j.

Equations

• Algebraic.Cutwidth.Gaussian.Internal.blockVertices H score c block j = {v : W | ∃ e ∈ H.edgeFinset, v ∈ e ∧ -c ≤ score e ∧ score e < c ∧ block e = j}

noncomputable def Algebraic.Cutwidth.Gaussian.Internal.blockLow {W : Type} [Fintype W] [DecidableEq W] (H : SimpleGraph W) [DecidableRel H.Adj] (score : Sym2 W → ℝ) (c : ℝ) (block : Sym2 W → ℕ) (j : ℕ) : Finset W

The endpoints of the band edges of block j with an edge scoring below -c.

Equations

• Algebraic.Cutwidth.Gaussian.Internal.blockLow H score c block j = {v : W | (∃ e ∈ H.edgeFinset, v ∈ e ∧ -c ≤ score e ∧ score e < c ∧ block e = j) ∧ ∃ e ∈ H.edgeFinset, v ∈ e ∧ score e < -c}

noncomputable def Algebraic.Cutwidth.Gaussian.Internal.blockHigh {W : Type} [Fintype W] [DecidableEq W] (H : SimpleGraph W) [DecidableRel H.Adj] (score : Sym2 W → ℝ) (c : ℝ) (block : Sym2 W → ℕ) (j : ℕ) : Finset W

The endpoints of the band edges of block j with an edge scoring at least c.

Equations

• Algebraic.Cutwidth.Gaussian.Internal.blockHigh H score c block j = {v : W | (∃ e ∈ H.edgeFinset, v ∈ e ∧ -c ≤ score e ∧ score e < c ∧ block e = j) ∧ ∃ e ∈ H.edgeFinset, v ∈ e ∧ c ≤ score e}

noncomputable def Algebraic.Cutwidth.Gaussian.Internal.blockImbalance {W : Type} [Fintype W] [DecidableEq W] (H : SimpleGraph W) [DecidableRel H.Adj] (score : Sym2 W → ℝ) (c : ℝ) (block : Sym2 W → ℕ) (j : ℕ) : ℤ

The imbalance B_j - A_j of block j.

Equations

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

noncomputable def Algebraic.Cutwidth.Gaussian.Internal.blockRank {W : Type} [Fintype W] [DecidableEq W] (H : SimpleGraph W) [DecidableRel H.Adj] (score : Sym2 W → ℝ) (c : ℝ) (block : Sym2 W → ℕ) (j : ℕ) : ℕ

The rank of block j among the band labels, ordered by imbalance and then by label.

Equations

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

noncomputable def Algebraic.Cutwidth.Gaussian.Internal.blockValue {W : Type} [Fintype W] [DecidableEq W] (H : SimpleGraph W) [DecidableRel H.Adj] (score : Sym2 W → ℝ) (c : ℝ) (block : Sym2 W → ℕ) (j : ℕ) : ℝ

The value of block j, strictly between -c and c and increasing with its rank.

Equations

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

noncomputable def Algebraic.Cutwidth.Gaussian.Internal.bandScore {W : Type} (score : Sym2 W → ℝ) (c : ℝ) (block : Sym2 W → ℕ) (val : ℕ → ℝ) (e : Sym2 W) : ℝ

The band-jump score: a band edge gets the value of its block, every other edge keeps its score.

Equations

• Algebraic.Cutwidth.Gaussian.Internal.bandScore score c block val e = if -c ≤ score e ∧ score e < c then val (block e) else score e

theorem Algebraic.Cutwidth.Gaussian.Internal.bandScore_of_mem {W : Type} {score : Sym2 W → ℝ} {c : ℝ} {block : Sym2 W → ℕ} {val : ℕ → ℝ} {e : Sym2 W} (h : -c ≤ score e ∧ score e < c) : bandScore score c block val e = val (block e)

theorem Algebraic.Cutwidth.Gaussian.Internal.bandScore_of_not_mem {W : Type} {score : Sym2 W → ℝ} {c : ℝ} {block : Sym2 W → ℕ} {val : ℕ → ℝ} {e : Sym2 W} (h : ¬(-c ≤ score e ∧ score e < c)) : bandScore score c block val e = score e

theorem Algebraic.Cutwidth.Gaussian.Internal.eq_of_touches {W : Type} [Fintype W] [DecidableEq W] (H : SimpleGraph W) [DecidableRel H.Adj] {score : Sym2 W → ℝ} {c : ℝ} {block : Sym2 W → ℕ} (hblock : BandBlocks H score c block) {v : W} {i j : ℕ} (hi : ∃ e ∈ H.edgeFinset, v ∈ e ∧ -c ≤ score e ∧ score e < c ∧ block e = i) (hj : ∃ e ∈ H.edgeFinset, v ∈ e ∧ -c ≤ score e ∧ score e < c ∧ block e = j) : i = j

Counting the straddling vertices

theorem Algebraic.Cutwidth.Gaussian.Internal.card_add_sum_le {W : Type} [DecidableEq W] {X T : Finset W} {L : Finset ℕ} {f : ℕ → Finset W} (hX : X ⊆ T) (hf : ∀ j ∈ L, f j ⊆ T) (hXf : ∀ j ∈ L, Disjoint X (f j)) (hff : ∀ i ∈ L, ∀ j ∈ L, i ≠ j → Disjoint (f i) (f j)) : X.card + ∑ j ∈ L, (f j).card ≤ T.card

Disjoint pieces of T have total size at most |T|.

theorem Algebraic.Cutwidth.Gaussian.Internal.card_bandFree_add_sum_blockLow_le {W : Type} [Fintype W] [DecidableEq W] (H : SimpleGraph W) [DecidableRel H.Adj] {score : Sym2 W → ℝ} {c : ℝ} {block : Sym2 W → ℕ} (hc : 0 ≤ c) (hblock : BandBlocks H score c block) : (bandFree H score c).card + ∑ j ∈ bandLabels H score c block, (blockLow H score c block j).card ≤ {v : W | EdgeStraddles H score (-c) v}.card

The vertices straddling -c contain the band-free ones and, disjointly, the low endpoints of every block.

theorem Algebraic.Cutwidth.Gaussian.Internal.card_bandFree_add_sum_blockHigh_le {W : Type} [Fintype W] [DecidableEq W] (H : SimpleGraph W) [DecidableRel H.Adj] {score : Sym2 W → ℝ} {c : ℝ} {block : Sym2 W → ℕ} (hc : 0 ≤ c) (hblock : BandBlocks H score c block) : (bandFree H score c).card + ∑ j ∈ bandLabels H score c block, (blockHigh H score c block j).card ≤ {v : W | EdgeStraddles H score c v}.card

The vertices straddling c contain the band-free ones and, disjointly, the high endpoints of every block.

The band-jump score

theorem Algebraic.Cutwidth.Gaussian.Internal.scoreSpan_bandScore_subset {W : Type} [Fintype W] [DecidableEq W] (H : SimpleGraph W) [DecidableRel H.Adj] {score : Sym2 W → ℝ} {c : ℝ} {block : Sym2 W → ℕ} {val : ℕ → ℝ} (hval : ∀ (j : ℕ), -c < val j ∧ val j < c) {t : ℝ} (ht : t < -c ∨ c ≤ t) : scoreSpan H (bandScore score c block val) t ⊆ scoreSpan H score t

Outside the band, the band-jump score only removes vertices.

theorem Algebraic.Cutwidth.Gaussian.Internal.card_scoreSpan_bandScore_le {W : Type} [Fintype W] [DecidableEq W] (H : SimpleGraph W) [DecidableRel H.Adj] {score : Sym2 W → ℝ} {c : ℝ} {block : Sym2 W → ℕ} (hblock : BandBlocks H score c block) (val : ℕ → ℝ) (hinj : ∀ i ∈ bandLabels H score c block, ∀ j ∈ bandLabels H score c block, val i = val j → i = j) (hmono : ∀ i ∈ bandLabels H score c block, ∀ j ∈ bandLabels H score c block, val i < val j → blockImbalance H score c block i ≤ blockImbalance H score c block j) {t : ℝ} (ht : -c ≤ t) (ht' : t < c) : ∃ (j : ℕ), (scoreSpan H (bandScore score c block val) t).card ≤ (bandFree H score c).card + max (∑ i ∈ bandLabels H score c block, (blockLow H score c block i).card) (∑ i ∈ bandLabels H score c block, (blockHigh H score c block i).card) + (blockVertices H score c block j).card

Inside the band, a vertex with a jumped score at most t and one at least t is band-free, a high endpoint of a block valued below t, a low endpoint of a block valued above t, or an endpoint of the block valued t.

Block values

theorem Algebraic.Cutwidth.Gaussian.Internal.blockValue_lt_blockValue {W : Type} [Fintype W] [DecidableEq W] (H : SimpleGraph W) [DecidableRel H.Adj] (score : Sym2 W → ℝ) (c : ℝ) (block : Sym2 W → ℕ) (hc : 0 < c) {i j : ℕ} (h : blockRank H score c block i < blockRank H score c block j) : blockValue H score c block i < blockValue H score c block j

theorem Algebraic.Cutwidth.Gaussian.Internal.blockValue_mem {W : Type} [Fintype W] [DecidableEq W] (H : SimpleGraph W) [DecidableRel H.Adj] (score : Sym2 W → ℝ) (c : ℝ) (block : Sym2 W → ℕ) (hc : 0 < c) (j : ℕ) : -c < blockValue H score c block j ∧ blockValue H score c block j < c

theorem Algebraic.Cutwidth.Gaussian.Internal.blockRank_lt_of_blockValue_lt {W : Type} [Fintype W] [DecidableEq W] (H : SimpleGraph W) [DecidableRel H.Adj] (score : Sym2 W → ℝ) (c : ℝ) (block : Sym2 W → ℕ) (hc : 0 < c) {i j : ℕ} (h : blockValue H score c block i < blockValue H score c block j) : blockRank H score c block i < blockRank H score c block j

theorem Algebraic.Cutwidth.Gaussian.Internal.blockImbalance_le_of_blockValue_lt {W : Type} [Fintype W] [DecidableEq W] (H : SimpleGraph W) [DecidableRel H.Adj] (score : Sym2 W → ℝ) (c : ℝ) (block : Sym2 W → ℕ) (hc : 0 < c) {i j : ℕ} (h : blockValue H score c block i < blockValue H score c block j) : blockImbalance H score c block i ≤ blockImbalance H score c block j

theorem Algebraic.Cutwidth.Gaussian.Internal.eq_of_blockValue_eq {W : Type} [Fintype W] [DecidableEq W] (H : SimpleGraph W) [DecidableRel H.Adj] (score : Sym2 W → ℝ) (c : ℝ) (block : Sym2 W → ℕ) (hc : 0 < c) {i j : ℕ} (hi : i ∈ bandLabels H score c block) (hj : j ∈ bandLabels H score c block) (h : blockValue H score c block i = blockValue H score c block j) : i = j

The band-jump decomposition

theorem Algebraic.Cutwidth.Gaussian.Internal.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 : BandBlocks H score c block) {B : ℝ} (outside : ∀ (t : ℝ), t < -c ∨ c ≤ t → ↑(scoreSpan H score t).card ≤ B) (inside : ∀ (j : ℕ), ↑{v : W | EdgeStraddles H score (-c) v}.card + ↑(blockVertices H score c block j).card ≤ B ∧ ↑{v : W | EdgeStraddles H score c v}.card + ↑(blockVertices H score c block j).card ≤ B) : ∃ (D : PathDecomposition H), ∀ (k : Fin D.length), ↑(D.bag k).card ≤ B

Band-jump path decomposition. The score-order decomposition of the band-jump score bandScore score c block (blockValue H score c block): bags at thresholds outside the band are bounded by outside, and bags inside it by inside for the block valued at the threshold.

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

Outside the band, thresholds come from a low grid reaching -c, a high grid starting at or below c, and the two tails.