The density of the core of a saturated compression

Let G be a connected multigraph of maximum degree d, with N vertices, M edges and cycle rank β₁ = M - N + 1, and let a saturated compression of G with budget d have at least two blocks. Its quotient, the core, is a loopless multigraph of maximum degree d in which:

• the ends of every edge have at least d + 3 edges between them, counted with multiplicity, since more than d edges leave their union and the edges between them are counted twice (Saturated.add_three_le_ncard_incidenceSet_quotient);
• hence every block has at least three edges (Saturated.three_le_ncard_incidenceSet_quotient).

By the density of cores (Cslib.Circuits.Frontier.Multigraph.core_density), 3 d |blocks| ≤ (d + 3) |E(core)|, and with the counting invariant of compressions, |E(core)| - |blocks| ≤ β₁ - 1, this gives (2d - 3) |E(core)| ≤ 3 d β₁ (Saturated.mul_card_external_le).

Main results

• Cslib.Circuits.Frontier.Multigraph.Compression.Saturated.three_le_ncard_incidenceSet_quotient: the blocks of the core have at least three edges.
• Cslib.Circuits.Frontier.Multigraph.Compression.Saturated.card_blocks_le_card_external: the core has at least as many edges as blocks.
• Cslib.Circuits.Frontier.Multigraph.Compression.Saturated.mul_card_external_le: the core has at most 3 d β₁ / (2d - 3) edges.

theorem Cslib.Circuits.Frontier.Multigraph.Compression.mem_external_of_mem_edgeCut {V : Type u_1} {E : Type u_2} {G : Multigraph V E} {d : ℕ} {c : G.Compression d} {B : ↥c.blocks} {e : E} (he : e ∈ G.edgeCut {v : V | v ∈ ↑B}) : e ∈ c.external

An edge leaving a block is external.

theorem Cslib.Circuits.Frontier.Multigraph.Compression.Saturated.add_three_le_ncard_incidenceSet_quotient {V : Type u_1} {E : Type u_2} {G : Multigraph V E} {d : ℕ} {c : G.Compression d} [Finite E] (hc : c.Saturated) (e : ↑c.external) : d + 3 ≤ (c.quotient.incidenceSet (c.quotient.src e)).ncard + (c.quotient.incidenceSet (c.quotient.tgt e)).ncard

In a saturated compression, the ends of an edge of the quotient have at least d + 3 edges between them: more than d edges leave their union, and the edges between them are counted twice.

theorem Cslib.Circuits.Frontier.Multigraph.Compression.Saturated.three_le_ncard_incidenceSet_quotient {V : Type u_1} {E : Type u_2} {G : Multigraph V E} {d : ℕ} {c : G.Compression d} [Finite E] (hc : c.Saturated) (hG : G.toSimpleGraph.Connected) (two : 1 < Nat.card ↥c.blocks) (B : ↥c.blocks) : 3 ≤ (c.quotient.incidenceSet B).ncard

In a saturated compression of a connected multigraph into at least two blocks, every block has at least three edges in the quotient.

theorem Cslib.Circuits.Frontier.Multigraph.Compression.Saturated.card_blocks_le_card_external {V : Type u_1} {E : Type u_2} {G : Multigraph V E} {d : ℕ} {c : G.Compression d} [Finite E] (hc : c.Saturated) (hG : G.toSimpleGraph.Connected) (two : 1 < Nat.card ↥c.blocks) : Nat.card ↥c.blocks ≤ Nat.card ↑c.external

A saturated compression of a connected multigraph into at least two blocks has at least as many external edges as blocks.

theorem Cslib.Circuits.Frontier.Multigraph.Compression.Saturated.mul_card_external_le {V : Type u_1} {E : Type u_2} {G : Multigraph V E} {d : ℕ} {c : G.Compression d} [Finite E] (hc : c.Saturated) (hG : G.toSimpleGraph.Connected) (two : 1 < Nat.card ↥c.blocks) : (2 * d - 3) * Nat.card ↑c.external ≤ 3 * d * G.cycleRank

The density of the core. A saturated compression with budget d of a connected multigraph into at least two blocks has at most 3 d / (2d - 3) times the cycle rank of the multigraph external edges: (2d - 3) |E(core)| ≤ 3 d β₁.