Grace/Cumulus/GraphTheory/TreePacking/Corollaries.g17

Open in Workbench Download source

Imports

Kaiser · Multigraph.Doubling · Combinatorics.Partitions

Declarations

Source

1-- Consequences of tree packing: a 2k-edge-connected graph has k disjoint2-- spanning trees, and a 3-edge-connected graph has three spanning trees with3-- no edge common to all three, found in the graph with every edge doubled.4-- Part of Cumulus, the Grace17 mathematics library.5-- Copyright (c) 2026 Grant Passmore.6-- Released under the Apache License 2.0. See LICENSE in the repository root.7-- Authors: Grant Passmore89module Grace.Cumulus.GraphTheory.TreePacking.Corollaries10import Kaiser11import Multigraph.Doubling12import Combinatorics.Partitions1314-- Section: The cut of a class and its degree in the quotient.1516-- An edge leaving a class of P joins two classes.17theorem crossingClasses.of_crossing (V E P leftEnd rightEnd X g : Set)18  requires graph : Graph(V, E, leftEnd, rightEnd)19  requires partition : Partition(V, P)20  requires class : X ∈ P21  requires cut : g ∈ crossing(leftEnd, rightEnd, E, X)22  shows g ∈ crossingClasses(P, leftEnd, rightEnd, E)23proof24  obtain ⟨inE, sides⟩ := cut25  obtain ⟨leftIn, rightIn⟩ := Graph.ends with graph, g, inE26  have leftIff := classOf.eq_iff_member with partition, class, leftIn27  have rightIff := classOf.eq_iff_member with partition, class, rightIn28  refine ⟨inE, _⟩29  intro same30  rcases sides with ⟨leftX, rightX⟩ | ⟨rightX, leftX⟩31  . have leftClass := leftIff.backward with leftX32    rw same at leftClass33    exact rightX with (rightIff.forward with leftClass)34  . have rightClass := rightIff.backward with rightX35    rw ← same at rightClass36    exact leftX with (leftIff.forward with rightClass)3738-- An edge leaving the class X is, in the quotient, an end of a crossing edge39-- at X: the end on the side of X, which is the right end exactly when the40-- right end lies in X.41defgraph crossingEnd (V E P leftEnd rightEnd X : Set)42    (g ∈ crossing(leftEnd, rightEnd, E, X)) :43    incidentEnds(quotientEnd(E, P, leftEnd), quotientEnd(E, P, rightEnd),44      crossingClasses(P, leftEnd, rightEnd, E), X) :=45  (g, indicator(X, rightEnd(g)))46requires graph : Graph(V, E, leftEnd, rightEnd)47requires partition : Partition(V, P)48requires class : X ∈ P49proof50  have inE := member.left51  obtain ⟨leftIn, rightIn⟩ := Graph.ends with graph, g, inE52  obtain ⟨leftValue, rightValue⟩ :=53    quotientEnd.value with graph, partition, inE54  have crossing :=55    crossingClasses.of_crossing with graph, partition, class, member56  have leftIff := classOf.eq_iff_member with partition, class, leftIn57  have rightIff := classOf.eq_iff_member with partition, class, rightIn58  rw incidentEnds.pair59  refine ⟨crossing, _⟩60  rw [leftValue, rightValue]61  rcases member.right with ⟨leftX, rightX⟩ | ⟨rightX, leftX⟩62  . left63    rw indicator.absent with rightX64    exact ⟨rfl, (leftIff.backward with leftX)⟩65  . right66    rw indicator.member with rightX67    exact ⟨rfl, (rightIff.backward with rightX)⟩6869theorem crossingEnd.injective (V E P leftEnd rightEnd X : Set)70  requires graph : Graph(V, E, leftEnd, rightEnd)71  requires partition : Partition(V, P)72  requires class : X ∈ P73  shows InjectiveBetween(crossingEnd(V, E, P, leftEnd, rightEnd, X),74    crossing(leftEnd, rightEnd, E, X),75    incidentEnds(quotientEnd(E, P, leftEnd), quotientEnd(E, P, rightEnd),76      crossingClasses(P, leftEnd, rightEnd, E), X))77proof78  have function := crossingEnd.function at V, E, P, leftEnd, rightEnd, X79    with graph, partition, class80  apply Injective.of_pointwise with function81  intros g hg h hh same82  rw [(crossingEnd.value at V, E, P, leftEnd, rightEnd, X, g83      with graph, partition, class, hg),84    (crossingEnd.value at V, E, P, leftEnd, rightEnd, X, h85      with graph, partition, class, hh)] at same86  exact orderedPair.first with same8788-- So the cut of a class is no larger than its degree in the quotient.89theorem degreeIn.quotient_ge_cut (V E P leftEnd rightEnd X : Set)90  requires graph : Graph(V, E, leftEnd, rightEnd)91  requires finiteEdges : Finite(E)92  requires partition : Partition(V, P)93  requires class : X ∈ P94  shows cardinality(crossing(leftEnd, rightEnd, E, X)) ≤95    degreeIn(quotientEnd(E, P, leftEnd), quotientEnd(E, P, rightEnd),96      crossingClasses(P, leftEnd, rightEnd, E), X)97proof98  have injective := crossingEnd.injective with graph, partition, class99  have finiteCut := crossing.finite at leftEnd, rightEnd, E, X100    with finiteEdges101  have finiteClasses := crossingClasses.finite102    at P, leftEnd, rightEnd, E with finiteEdges103  have image := cardinality.injective_image104    with injective, Subset.reflexive, finiteCut105  unfold degreeIn106  rw ← image107  exact cardinality.monotone108    with (incidentEnds.finite with finiteClasses), functionImage.subset109110-- Section: Edge-connectivity gives the packing condition.111112-- Summing the cut sizes over the classes of a partition counts each crossing113-- edge twice, so 2k-edge-connectivity gives the packing condition for k. The114-- sum is the degree sum of the crossing edges in the quotient graph, which115-- the handshake lemma evaluates.116theorem EdgeConnected.packing_condition (V E leftEnd rightEnd : Set, k : Nat)117  requires graph : Graph(V, E, leftEnd, rightEnd)118  requires finiteVertices : Finite(V)119  requires finiteEdges : Finite(E)120  requires connected : EdgeConnected(V, E, leftEnd, rightEnd, 2 * k)121  shows PackingCondition(V, E, leftEnd, rightEnd, k)122proof123  intros P partition124  have finiteP := Partition.finite with finiteVertices, partition125  have finiteClasses := crossingClasses.finite126    at P, leftEnd, rightEnd, E with finiteEdges127  have natClasses := cardinality.nat with finiteClasses128  have natP := cardinality.nat with finiteP129  by_cases whole : V ∈ P130  . -- The trivial partition has one class and asks for nothing.131    have single : P = {V}132      ext Y133      constructor134      . intro hY135        rw singleton.membership136        by_contra different137        have apart := partition.right.left with Y, hY, V, whole, different138        obtain ⟨inV, nonempty⟩ := partition.left with Y, hY139        obtain ⟨y, hy⟩ := Nonempty.of_ne_empty with nonempty140        rw Disjoint.iff at apart141        exact apart with y, hy, (inV with y, hy)142      . intro hY143        rw singleton.membership at hY144        rw hY145        exact whole146    have zero : k * (1 - 1) = 0147      have one : 1 - 1 = 0 by compute148      rw one149      ring150    have count : cardinality(P) = 1151      rw single152      exact cardinality.singleton153    rw [count, zero]154    arith155  . -- Every class is a nonempty proper vertex set, left by at least 2k156    -- edges, and the degree of a class in the quotient is at least its cut.157    have edgesClasses : crossingClasses(P, leftEnd, rightEnd, E) ⊆ E :=158      crossingClasses.subset159    have endsQ := quotientEnd.ends with graph, partition, edgesClasses160    have handshake := degreeIn.handshake with finiteP, finiteClasses, endsQ161    have bounds : ∀ X ∈ P,162        degreeWeights(P, quotientEnd(E, P, leftEnd),163          quotientEnd(E, P, rightEnd),164          crossingClasses(P, leftEnd, rightEnd, E))(X) ∈ ℕ ∧165        LessEqual(2 * k, degreeWeights(P, quotientEnd(E, P, leftEnd),166          quotientEnd(E, P, rightEnd),167          crossingClasses(P, leftEnd, rightEnd, E))(X))168      intros X hX169      obtain ⟨inV, nonempty⟩ := partition.left with X, hX170      have proper : X ≠ V171        intro same172        rw same at hX173        exact whole with hX174      have many := connected with X, inV, nonempty, proper175      have below := degreeIn.quotient_ge_cut176        with graph, finiteEdges, partition, hX177      have natDegree := degreeIn.natural178        at quotientEnd(E, P, leftEnd), quotientEnd(E, P, rightEnd),179          crossingClasses(P, leftEnd, rightEnd, E), X180        with finiteClasses181      rw degreeWeights.value with finiteClasses, hX182      refine ⟨natDegree, _⟩183      arith184    have lower := natSum.ge_of_bounded with finiteP, bounds185    rw handshake at lower186    -- Cancel the factor two, then drop one class.187    have rearranged : cardinality(P) * (2 * k) = 2 * (k * cardinality(P))188      ring189    rw rearranged at lower190    have twoPositive : 2 ≠ 0 by simp191    have cancelled :=192      LessEqual.mul_left_cancel_positive with twoPositive, lower193    have step : cardinality(P) ≤ cardinality(P) + 1 by arith194    have below := sub.one_le_of_le_add_one with step195    have monotone := LessEqual.mul_left196      at cardinality(P) - 1, cardinality(P), k with below197    exact LessEqual.transitive with monotone, cancelled198199theorem EdgeConnected.tree_packing (V E leftEnd rightEnd : Set, k : Nat)200  requires graph : Graph(V, E, leftEnd, rightEnd)201  requires finiteVertices : Finite(V)202  requires finiteEdges : Finite(E)203  requires nonempty : V ≠ ∅204  requires connected : EdgeConnected(V, E, leftEnd, rightEnd, 2 * k)205  shows TreePacking(V, E, leftEnd, rightEnd, k)206proof207  have condition := EdgeConnected.packing_condition208    with graph, finiteVertices, finiteEdges, connected209  exact treePacking with graph, finiteVertices, finiteEdges, nonempty, condition210211-- Section: Three spanning trees with no common edge.212213-- Three spanning trees of the doubled graph correspond to three spanning214-- trees of G, and no edge of G lies in all three: the projection of a tree215-- connects V, since a vertex set closed under the projected edges is closed216-- under their copies, and has at most |V| − 1 edges; an edge of all three217-- projections would have two copies in one tree, as there are two sides.218theorem EdgeConnected.three_trees (V E leftEnd rightEnd : Set)219  requires graph : Graph(V, E, leftEnd, rightEnd)220  requires finiteVertices : Finite(V)221  requires finiteEdges : Finite(E)222  requires nonempty : V ≠ ∅223  requires connected : EdgeConnected(V, E, leftEnd, rightEnd, 3)224  shows ∃ T, FunctionBetween(T, 3, 𝒫(E)) ∧225    (∀ i ∈ 3, SpanningTree(V, leftEnd, rightEnd, T(i))) ∧226    T(0) ∩ T(1) ∩ T(2) = ∅227proof228  have doubledGraph := doubled.graph with graph229  have doubledConnected :=230    doubled.edge_connected with graph, finiteEdges, connected231  have finiteDoubled : Finite(doubledEdges(E))232    unfold doubledEdges233    exact Finite.product with finiteEdges, Finite.natural234  obtain ⟨T, function, apart, trees⟩ := EdgeConnected.tree_packing235    with doubledGraph, finiteVertices, finiteDoubled, nonempty, doubledConnected236  have endsE := Graph.ends with graph237  have natV := cardinality.nat with finiteVertices238  -- Each tree projects to a spanning tree of G.239  have spanning : ∀ i ∈ 3,240      SpanningTree(V, leftEnd, rightEnd, projected(E, T(i)))241    intros i hi242    have tree := trees with i, hi243    have inDoubled : T(i) ⊆ doubledEdges(E) := powerset.membership_iff.forward244      with (FunctionBetween.apply_closed with function, hi)245    unfold doubledEdges at inDoubled246    have inE : projected(E, T(i)) ⊆ E247      intros e he248      exact he.left249    have finiteProjected := Finite.subset with finiteEdges, inE250    have connects : Connects(V, leftEnd, rightEnd, projected(E, T(i)))251      intros u hu v hv A start closed252      have closedCopies : ClosedUnder(doubledEnd(V, E, leftEnd),253          doubledEnd(V, E, rightEnd), T(i), A)254        intros p hp255        obtain ⟨_, e, he, j, hj, rfl⟩ :=256          product.membership.forward with (inDoubled with p, hp)257        rw [(doubledEnd.value with graph.left, he, hj),258          (doubledEnd.value with graph.right, he, hj)]259        exact closed with e, ⟨he, j, hj, hp⟩260      have joined := tree.right.left with u, hu, v, hv261      exact joined with A, start, closedCopies262    have upper := projected.count with finiteEdges, inDoubled263    have lower := componentsBy.lower_bound264      with finiteVertices, finiteProjected, (ends_in.subset with endsE, inE)265    rw componentsBy.connected_count with connects, nonempty at lower266    have count := tree.right.right267    have natT := cardinality.nat with tree.left268    have natProjected := cardinality.nat with finiteProjected269    refine ⟨finiteProjected, connects, _⟩270    arith271  have less0 : 0 < 3 by arith272  have less1 : 1 < 3 by arith273  have less2 : 2 < 3 by arith274  have zero := membership.of_Less at 0, 3 with *, less0275  have one := membership.of_Less at 1, 3 with *, less1276  have two := membership.of_Less at 2, 3 with *, less2277  witness projectedTrees(E, T)278  refine ⟨(projectedTrees.function at E, T), _, _⟩279  . intros i hi280    rw projectedTrees.value with hi281    exact spanning with i, hi282  . -- An edge of all three projections has copies in three trees with only283    -- two sides, so two copies coincide, against the disjointness of trees.284    rw [(projectedTrees.value with zero), (projectedTrees.value with one),285      (projectedTrees.value with two)]286    have ne01 : 0 ≠ 1 by simp287    have ne02 : 0 ≠ 2 by simp288    have ne12 : 1 ≠ 2 by simp289    have apart01 := Disjoint.iff.forward with (apart with 0, zero, 1, one, ne01)290    have apart02 := Disjoint.iff.forward with (apart with 0, zero, 2, two, ne02)291    have apart12 := Disjoint.iff.forward with (apart with 1, one, 2, two, ne12)292    ext e293    constructor294    . intro he295      obtain ⟨both, in2⟩ := intersection.membership.forward with he296      obtain ⟨in0, in1⟩ := intersection.membership.forward with both297      obtain ⟨_, j0, hj0, c0⟩ := in0298      obtain ⟨_, j1, hj1, c1⟩ := in1299      obtain ⟨_, j2, hj2, c2⟩ := in2300      have cases0 := membership.two.forward with hj0301      have cases1 := membership.two.forward with hj1302      have cases2 := membership.two.forward with hj2303      exfalso304      rcases cases0 with rfl | rfl305      . rcases cases1 with rfl | rfl306        . exact apart01 with (e, 0), c0, c1307        . rcases cases2 with rfl | rfl308          . exact apart02 with (e, 0), c0, c2309          . exact apart12 with (e, 1), c1, c2310      . rcases cases1 with rfl | rfl311        . rcases cases2 with rfl | rfl312          . exact apart12 with (e, 0), c1, c2313          . exact apart02 with (e, 1), c0, c2314        . exact apart01 with (e, 1), c0, c1315    . intro he316      simp at he317