Grace/Cumulus/GraphTheory/Flows/EightFlow.g17

Open in Workbench Download source

Imports

Splits

Declarations

Source

1-- Every finite bridgeless multigraph has an even cover: the eight-flow2-- theorem of Jaeger and Kilpatrick, by induction on the number of vertices3-- through cuts of size zero and two, with three spanning trees in the4-- 3-edge-connected case.5-- Part of Cumulus, the Grace17 mathematics library.6-- Copyright (c) 2026 Grant Passmore.7-- Released under the Apache License 2.0. See LICENSE in the repository root.8-- Authors: Grant Passmore910module Grace.Cumulus.GraphTheory.Flows.EightFlow11import Splits1213-- Section: The cases of the induction.1415-- A bridgeless graph that is neither split nor 3-edge-connected has a cut of16-- exactly two edges, and both of its edges are proper.17theorem Bridgeless.two_cut (V E leftEnd rightEnd : Set)18  requires graph : Graph(V, E, leftEnd, rightEnd)19  requires finiteVertices : Finite(V)20  requires finiteEdges : Finite(E)21  requires bridgeless : Bridgeless(V, E, leftEnd, rightEnd)22  requires unsplit : ∀ X ⊆ V, X ≠ ∅ → X ≠ V →23    crossing(leftEnd, rightEnd, E, X) ≠ ∅24  requires loose : ¬EdgeConnected(V, E, leftEnd, rightEnd, 3)25  shows ∃ X, ∃ e ∈ E, ∃ f ∈ E, X ⊆ V ∧ e ≠ f ∧26    crossing(leftEnd, rightEnd, E, X) = {e, f}27proof28  -- Some nonempty proper vertex set is left by fewer than three edges.29  have witnessX : ∃ X ⊆ V, X ≠ ∅ ∧ X ≠ V ∧30      ¬(3 ≤ cardinality(crossing(leftEnd, rightEnd, E, X)))31    by_contra none32    apply loose33    intros X bound nonempty proper34    by_contra few35    exact none with ⟨X, bound, nonempty, proper, few⟩36  obtain ⟨X, bound, nonempty, proper, few⟩ := witnessX37  have finiteCut := crossing.finite at leftEnd, rightEnd, E, X with finiteEdges38  have natCut := cardinality.nat with finiteCut39  have notOne := bridgeless with X, bound40  have notZero : cardinality(crossing(leftEnd, rightEnd, E, X)) ≠ 041    intro zero42    exact unsplit with X, bound, nonempty, proper,43      (cardinality.eq_empty_of_zero with finiteCut, zero)44  -- Neither zero, one, nor three or more: the cut has exactly two edges.45  have less := Less.of_not_LessEqual with few46  have upper : cardinality(crossing(leftEnd, rightEnd, E, X)) ≤ 2 by arith47  have lower : 2 ≤ cardinality(crossing(leftEnd, rightEnd, E, X))48    have cases := natural.zero_one_or_above_one49      at cardinality(crossing(leftEnd, rightEnd, E, X))50    rcases cases with zero | one | above51    . exfalso52      exact notZero with zero53    . exfalso54      exact notOne with one55    . have strict := Less.of_membership with above56      arith57  have two := LessEqual.antisymmetric with upper, lower58  -- One edge of the cut, and the rest is a single other edge.59  have positive : 0 < cardinality(crossing(leftEnd, rightEnd, E, X)) by arith60  obtain ⟨e, he⟩ := cardinality.member_of_positive with finiteCut, positive61  have removed := cardinality.remove_add_one with finiteCut, he62  have oneLeft : cardinality(crossing(leftEnd, rightEnd, E, X) ∖ {e}) = 163    arith64  have finiteRest := Finite.difference65    at crossing(leftEnd, rightEnd, E, X), {e} with finiteCut66  have oneIff := cardinality.one_iff with finiteRest67  obtain ⟨f, single⟩ := oneIff.forward with oneLeft68  have fMember : f ∈ crossing(leftEnd, rightEnd, E, X) ∖ {e}69    rw single70    exact singleton.self71  obtain ⟨fIn, fNotE⟩ := difference.membership.forward with fMember72  have distinct : e ≠ f73    intro same74    apply fNotE75    rw same76    exact singleton.self77  have cutEdges := crossing.subset at leftEnd, rightEnd, E, X78  refine ⟨X, e, (cutEdges with e, he), f, (cutEdges with f, fIn),79    bound, distinct, _⟩80  ext g81  constructor82  . intro hg83    by_cases ge : g = e84    . simp [ge]85    . have inRest : g ∈ crossing(leftEnd, rightEnd, E, X) ∖ {e}86        simp [hg, ge]87      rw single at inRest88      simp at inRest89      simp [inRest]90  . intro hg91    simp at hg92    rcases hg with rfl | rfl93    . exact he94    . exact fIn9596-- One vertex: every edge is a loop and E itself is an even set.97theorem EvenCover.single_vertex (V E leftEnd rightEnd : Set)98  requires graph : Graph(V, E, leftEnd, rightEnd)99  requires finiteEdges : Finite(E)100  requires single : ∃ v, V = {v}101  shows ∃ F, EvenCover(V, E, leftEnd, rightEnd, F)102proof103  obtain ⟨v, rfl⟩ := single104  have endsE := Graph.ends with graph105  have vertex : v ∈ {v} := singleton.self106  -- Every edge is a loop at v, so E is even: its degree at v is 2|E|.107  have even : EvenEdgeSet({v}, leftEnd, rightEnd, E)108    constructor109    . exact finiteEdges110    . intros w hw111      rw singleton.membership at hw112      rw hw113      have sum := degreeIn.handshake114        with (Finite.singleton at v), finiteEdges, endsE115      have weights := degreeWeights.natural at {v}, leftEnd, rightEnd, E116        with finiteEdges117      rw [(natSum.singleton with (weights with v, vertex)),118        (degreeWeights.value with finiteEdges, vertex)] at sum119      rw sum120      exact Even.two_mul121  have member : E ∈ 𝒫(E) :=122    powerset.membership_iff.backward with Subset.reflexive123  have values := tripleMap.value with member, member, member124  have zero : 0 ∈ 3 by simp [membership.three]125  witness tripleMap(𝒫(E), E, E, E)126  refine ⟨(tripleMap.function with member, member, member), _, _⟩127  . intros i hi128    have cases := membership.three.forward with hi129    rcases cases with rfl | rfl | rfl130    . rw values.left131      exact even132    . rw values.right.left133      exact even134    . rw values.right.right135      exact even136  . intros e he137    refine ⟨0, zero, _⟩138    rw values.left139    exact he140141-- Without vertices there are no edges, and the empty triple is a cover.142theorem EvenCover.of_no_vertices (V E leftEnd rightEnd : Set)143  requires graph : Graph(V, E, leftEnd, rightEnd)144  requires noVertices : V = ∅145  shows ∃ F, EvenCover(V, E, leftEnd, rightEnd, F)146proof147  have noEdges : E = ∅148    ext e149    constructor150    . intro he151      have inV := (Graph.ends with graph, e, he).left152      rw noVertices at inV153      simp at inV154    . intro he155      simp at he156  have member : ∅ ∈ 𝒫(E) :=157    powerset.membership_iff.backward with empty.subset158  have values := tripleMap.value with member, member, member159  witness tripleMap(𝒫(E), ∅, ∅, ∅)160  refine ⟨(tripleMap.function with member, member, member), _, _⟩161  . intros i hi162    have cases := membership.three.forward with hi163    rcases cases with rfl | rfl | rfl164    . rw values.left165      exact EvenEdgeSet.empty166    . rw values.right.left167      exact EvenEdgeSet.empty168    . rw values.right.right169      exact EvenEdgeSet.empty170  . intros e he171    rw noEdges at he172    simp at he173174-- Section: The eight-flow theorem.175176-- A side of a split, with the ends restricted to its inside, is a finite177-- bridgeless graph on fewer vertices; the induction hypothesis covers it, and178-- the cover is one for the original ends.179theorem eightFlow.side (V E leftEnd rightEnd X : Set, n : Nat)180  requires graph : Graph(V, E, leftEnd, rightEnd)181  requires finiteVertices : Finite(V)182  requires finiteEdges : Finite(E)183  requires bridgeless : Bridgeless(V, E, leftEnd, rightEnd)184  requires split : X ⊆ V ∧ crossing(leftEnd, rightEnd, E, X) = ∅185  requires proper : X ≠ V186  requires bound : cardinality(V) ≤ n + 1187  requires ih : ∀ W, ∀ D, ∀ leftW, ∀ rightW,188    Graph(W, D, leftW, rightW) → Finite(W) → Finite(D) →189    Bridgeless(W, D, leftW, rightW) → cardinality(W) ≤ n →190    ∃ F, EvenCover(W, D, leftW, rightW, F)191  shows ∃ F, EvenCover(X, inside(leftEnd, rightEnd, E, X), leftEnd, rightEnd,192    F)193proof194  have edges := inside.subset at leftEnd, rightEnd, E, X195  have sideGraph := inside.graph with graph, split.left196  have sideBridgeless := inside.bridgeless with graph, split, bridgeless197  have finiteX := Finite.subset with finiteVertices, split.left198  have finiteInside := Finite.subset with finiteEdges, edges199  have less := cardinality.strict_of_ne with finiteVertices, split.left, proper200  have smaller : cardinality(X) ≤ n by arith201  have recursive := ih with X, inside(leftEnd, rightEnd, E, X),202    restrict(leftEnd, inside(leftEnd, rightEnd, E, X)),203    restrict(rightEnd, inside(leftEnd, rightEnd, E, X))204  obtain ⟨F, cover⟩ := recursive205    with sideGraph, finiteX, finiteInside, sideBridgeless, smaller206  exact ⟨F, (EvenCover.of_restricted with graph, edges, cover)⟩207208-- The theorem, by induction on the number of vertices: a split joins the209-- covers of its two sides, a cut of two edges contracts one of them to a210-- graph with one vertex fewer, and otherwise the graph is 3-edge-connected.211theorem eightFlow.of_vertex_count (n : Nat)212  shows ∀ V, ∀ E, ∀ leftEnd, ∀ rightEnd,213    Graph(V, E, leftEnd, rightEnd) → Finite(V) → Finite(E) →214    Bridgeless(V, E, leftEnd, rightEnd) → cardinality(V) ≤ n →215    ∃ F, EvenCover(V, E, leftEnd, rightEnd, F)216proof217  induction n218  | zero =>219    intros V E leftEnd rightEnd graph finiteVertices finiteEdges bridgeless220      bound221    have natV := cardinality.nat with finiteVertices222    have zero : cardinality(V) = 0 by arith223    exact EvenCover.of_no_vertices224      with graph, (cardinality.eq_empty_of_zero with finiteVertices, zero)225  | k + 1 using ih =>226    intros V E leftEnd rightEnd graph finiteVertices finiteEdges bridgeless227      bound228    have endsE := Graph.ends with graph229    have natV := cardinality.nat with finiteVertices230    by_cases nonempty : V = ∅231    . exact EvenCover.of_no_vertices with graph, nonempty232    by_cases unsplit : ∀ X ⊆ V, X ≠ ∅ → X ≠ V →233      crossing(leftEnd, rightEnd, E, X) ≠ ∅234    . by_cases connected : EdgeConnected(V, E, leftEnd, rightEnd, 3)235      . exact EvenCover.of_three_edge_connected236          with graph, finiteVertices, finiteEdges, nonempty, connected237      . -- A cut of two edges: contract one of them and lift the cover.238        obtain ⟨X, e, eInE, f, fInE, subset, distinct, cut⟩ :=239          Bridgeless.two_cut with graph, finiteVertices, finiteEdges,240            bridgeless, unsplit, connected241        have eInCut : e ∈ crossing(leftEnd, rightEnd, E, X)242          rw cut243          exact pair.left244        have proper : leftEnd(e) ≠ rightEnd(e)245          intro same246          rcases eInCut.right with ⟨leftX, rightX⟩ | ⟨rightX, leftX⟩247          . rw same at leftX248            exact rightX with leftX249          . rw same at leftX250            exact leftX with rightX251        have count := contraction.vertex_count252          with graph, finiteVertices, eInE, proper253        have finiteClasses :254            Finite(contractionPartition(V, leftEnd, rightEnd, e))255          unfold contractionPartition256          exact componentsBy.finite with finiteVertices257        have natClasses := cardinality.nat with finiteClasses258        have smaller :259            cardinality(contractionPartition(V, leftEnd, rightEnd, e)) ≤ k260          arith261        have recursive := ih262          with contractionPartition(V, leftEnd, rightEnd, e), E ∖ {e},263            contractedLeft(V, E, leftEnd, rightEnd, e),264            contractedRight(V, E, leftEnd, rightEnd, e)265        obtain ⟨F, cover⟩ := recursive266          with (contraction.graph with graph, eInE), finiteClasses,267          (Finite.difference with finiteEdges),268          (contraction.bridgeless with graph, finiteEdges, eInE, bridgeless),269          smaller270        exact contraction.lift_cover with graph, finiteVertices, finiteEdges,271          ⟨subset, cut, distinct⟩, cover272    . -- A nonempty proper vertex set left by no edge: cover each side.273      have witnessX : ∃ X ⊆ V, X ≠ ∅ ∧ X ≠ V ∧274          crossing(leftEnd, rightEnd, E, X) = ∅275        by_contra none276        apply unsplit277        intros X inV nonemptyX properX split278        exact none with ⟨X, inV, nonemptyX, properX, split⟩279      obtain ⟨X, subsetX, nonemptyX, properX, none⟩ := witnessX280      have complement : V ∖ X ⊆ V ∧281          crossing(leftEnd, rightEnd, E, V ∖ X) = ∅282        refine ⟨difference.subset_left, _⟩283        rw crossing.complement with endsE284        exact none285      have properY : V ∖ X ≠ V286        intro same287        obtain ⟨v, hv⟩ := Nonempty.of_ne_empty with nonemptyX288        have inV := subsetX with v, hv289        rw ← same at inV290        exact (difference.membership.forward with inV).right with hv291      obtain ⟨F, coverX⟩ := eightFlow.side with graph, finiteVertices,292        finiteEdges, bridgeless, ⟨subsetX, none⟩, properX, bound, ih293      obtain ⟨G, coverY⟩ := eightFlow.side with graph, finiteVertices,294        finiteEdges, bridgeless, complement, properY, bound, ih295      exact EvenCover.join with graph, ⟨subsetX, none⟩, coverX, coverY296297theorem eightFlow (V E leftEnd rightEnd : Set)298  requires graph : Graph(V, E, leftEnd, rightEnd)299  requires finiteVertices : Finite(V)300  requires finiteEdges : Finite(E)301  requires bridgeless : Bridgeless(V, E, leftEnd, rightEnd)302  shows ∃ F, EvenCover(V, E, leftEnd, rightEnd, F)303proof304  have natV := cardinality.nat with finiteVertices305  have all := eightFlow.of_vertex_count at cardinality(V)306  exact all with V, E, leftEnd, rightEnd, graph, finiteVertices, finiteEdges,307    bridgeless, (LessEqual.reflexive at cardinality(V))308