Compressing graphs of maximum degree four

Merge adjacent blocks whenever their union has at most four outgoing edges. In the final quotient there are no parallel edges, degrees are three or four, and two degree-three vertices are never adjacent. Charging weight four to each degree-three endpoint and weight three to each degree-four endpoint gives 12 |V| ≤ 7 |E|. The compression invariant then gives 5 |E(quotient)| ≤ 12 β₁(original).

def Complexity.Frontier.Multigraph.Compression.Terminal {V : Type u_1} {E : Type u_2} {G : Multigraph V E} {d : ℕ} (c : G.Compression d) : Prop

No adjacent pair of blocks can still be merged within the degree budget.

Equations

• c.Terminal = ∀ B ∈ c.blocks, ∀ B' ∈ c.blocks, B ≠ B' → (G.cut {v : V | v ∈ B} ∩ G.cut {v : V | v ∈ B'}).Nonempty → d < (G.cut ({v : V | v ∈ B} ∪ {v : V | v ∈ B'})).ncard

theorem Complexity.Frontier.Multigraph.Compression.exists_terminal {V : Type u_1} {E : Type u_2} {G : Multigraph V E} {d : ℕ} [Finite V] [Finite E] (hG : G.MaxDegreeLE d) : ∃ (c : G.Compression d), c.Terminal

The block count strictly decreases with every merge, in every degree.

theorem Complexity.Frontier.Multigraph.Compression.Terminal.final {V : Type u_1} {E : Type u_2} {G : Multigraph V E} {d : ℕ} (c : G.Compression d) [Finite E] (hc : c.Terminal) (hd : d ≤ 4) : c.Final

Up to degree four the terminal quotient is simple, and each nonisolated block has at least three outgoing edges.

theorem Complexity.Frontier.Multigraph.Compression.degree_ge_three {V : Type u_1} {E : Type u_2} {G : Multigraph V E} {d : ℕ} (c : G.Compression d) [Finite E] (hc : c.Final) (hG : G.Connected) (two : 2 ≤ c.blocks.card) [c.quotient.LocallyFinite] (B : ↥c.blocks) : 3 ≤ c.quotient.degree B

theorem Complexity.Frontier.Multigraph.Compression.Terminal.adjacent_degree_sum {V : Type u_1} {E : Type u_2} {G : Multigraph V E} {d : ℕ} (c : G.Compression d) [Finite E] (hc : c.Terminal) (hf : c.Final) [c.quotient.LocallyFinite] {B B' : ↥c.blocks} (hBB' : c.quotient.Adj B B') : d + 3 ≤ c.quotient.degree B + c.quotient.degree B'

The degree sum at adjacent quotient vertices is at least d + 3.

theorem Complexity.Frontier.quartic_core_density {W : Type u_1} [Fintype W] (H : SimpleGraph W) [DecidableRel H.Adj] (hlo : ∀ (v : W), 3 ≤ H.degree v) (hhi : ∀ (v : W), H.degree v ≤ 4) (hadj : ∀ (u v : W), H.Adj u v → 7 ≤ H.degree u + H.degree v) : 12 * Fintype.card W ≤ 7 * H.edgeFinset.card

Endpoint charging for a simple graph with degrees three or four and no adjacent degree-three vertices. Each vertex contributes twelve and each edge contributes at most seven.

theorem Complexity.Frontier.Multigraph.Compression.Terminal.blocks_le_edges {V : Type u_1} {E : Type u_2} {G : Multigraph V E} (c : G.Compression 4) [Finite E] [Fintype ↑c.quotient.edgeSet] (hc : c.Terminal) (hG : G.Connected) (two : 2 ≤ c.blocks.card) : c.blocks.card ≤ c.quotient.edgeFinset.card

A nontrivial terminal degree-four quotient has no more vertices than edges.

theorem Complexity.Frontier.Multigraph.Compression.Terminal.edge_bound {V : Type u_1} {E : Type u_2} {G : Multigraph V E} (c : G.Compression 4) [Finite E] [Fintype ↑c.quotient.edgeSet] (hc : c.Terminal) (hG : G.Connected) (two : 2 ≤ c.blocks.card) : 5 * c.quotient.edgeFinset.card ≤ 12 * G.cycleRank

The compressed degree-four core has at most 12 β₁ / 5 edges.