Grace/Cumulus/GraphTheory/Flows/EvenCovers.g17

Open in Workbench Download source

Imports

Multigraph.Trees · TreePacking.Corollaries · Set.Function.Triples

Declarations

Source

1-- A nowhere-zero flow with values in the three-dimensional space over the2-- two-element field is three even edge sets that together cover every edge;3-- the value of an edge is the set of coordinates whose even set holds it.4-- Three spanning trees with no common edge give one.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.EvenCovers11import Multigraph.Trees12import TreePacking.Corollaries13import Set.Function.Triples1415-- Section: Even covers as nowhere-zero flows over the field of two elements16-- cubed.1718-- F assigns an even edge set to each coordinate i ∈ 3, and every edge lies19-- in one of them.20predicate EvenCover (V E leftEnd rightEnd F : Set) :=21  FunctionBetween(F, 3, 𝒫(E)) ∧22  (∀ i ∈ 3, EvenEdgeSet(V, leftEnd, rightEnd, F(i))) ∧23  (∀ e ∈ E, ∃ i ∈ 3, e ∈ F(i))2425-- The value of an edge: the coordinates whose even set holds it.26def flowValue (F e : Set) : Set := { i ∈ 3 | e ∈ F(i) }2728-- The ends at v whose edge carries coordinate i.29def coordinateEnds (leftEnd rightEnd E F v i : Set) : Set :=30  { p ∈ incidentEnds(leftEnd, rightEnd, E, v) | i ∈ flowValue(F, fst(p)) }3132theorem flowValue.nonzero (V E leftEnd rightEnd F e : Set)33  requires cover : EvenCover(V, E, leftEnd, rightEnd, F)34  requires edge : e ∈ E35  shows flowValue(F, e) ≠ ∅36proof37  obtain ⟨i, hi, member⟩ := cover.right.right with e, edge38  apply Nonempty.ne_empty39  witness i40  exact ⟨hi, member⟩4142-- The ends at v carrying coordinate i are the ends of the edges of F(i) at v.43theorem coordinateEnds.eq (V E leftEnd rightEnd F v i : Set)44  requires cover : EvenCover(V, E, leftEnd, rightEnd, F)45  requires coordinate : i ∈ 346  shows coordinateEnds(leftEnd, rightEnd, E, F, v, i) =47    incidentEnds(leftEnd, rightEnd, F(i), v)48proof49  have edges : F(i) ⊆ E := powerset.membership_iff.forward50    with (FunctionBetween.apply_closed with cover.left, coordinate)51  ext p52  constructor53  . intro hp54    obtain ⟨inEnds, value⟩ := hp55    obtain ⟨e, he, j, hj, rfl⟩ := incidentEnds.shape with inEnds56    rw fst.pair at value57    have atV := (incidentEnds.pair.forward with inEnds).right58    exact incidentEnds.pair.backward with ⟨value.right, atV⟩59  . intro hp60    obtain ⟨e, he, j, hj, rfl⟩ := incidentEnds.shape with hp61    have atV := (incidentEnds.pair.forward with hp).right62    have inE := edges with e, he63    refine ⟨(incidentEnds.pair.backward with ⟨inE, atV⟩), _⟩64    rw fst.pair65    exact ⟨coordinate, he⟩6667-- Conservation at a vertex: the values of the incident ends sum to zero,68-- coordinate by coordinate, since each even set has even degree there.69theorem flowValue.conservation (V E leftEnd rightEnd F v i : Set)70  requires cover : EvenCover(V, E, leftEnd, rightEnd, F)71  requires vertex : v ∈ V72  requires coordinate : i ∈ 373  shows EvenSet(coordinateEnds(leftEnd, rightEnd, E, F, v, i))74proof75  have even := (cover.right.left with i, coordinate).right with v, vertex76  unfold degreeIn at even77  unfold EvenSet78  rw coordinateEnds.eq with cover, coordinate79  exact even8081-- Section: An even set containing the complement of a spanning tree.8283-- Closing the edges of D outside the tree one at a time: the symmetric84-- difference of their fundamental even sets lies inside T ∪ D and holds85-- every edge of D, since the fundamental set of an edge holds no other edge86-- outside the tree.87theorem SpanningTree.even_superset_of (V E leftEnd rightEnd T D : Set)88  requires graph : Graph(V, E, leftEnd, rightEnd)89  requires finiteVertices : Finite(V)90  requires finite : Finite(D)91  requires tree : SpanningTree(V, leftEnd, rightEnd, T)92  requires edges : T ⊆ E93  requires outside : D ⊆ E ∖ T94  shows ∃ F ⊆ T ∪ D, EvenEdgeSet(V, leftEnd, rightEnd, F) ∧ D ⊆ F95proof96  induction finite with G a97  | empty =>98    exact ⟨∅, empty.subset, EvenEdgeSet.empty, empty.subset⟩99  | insert using ih =>100    obtain ⟨F, inside, even, covers⟩ := ih101    have endsE := Graph.ends with graph102    obtain ⟨aInE, aNotT⟩ := difference.membership.forward with aMember103    have ends : (∀ f ∈ T, leftEnd(f) ∈ V ∧ rightEnd(f) ∈ V)104        ∧ leftEnd(a) ∈ V ∧ rightEnd(a) ∈ V :=105      ⟨(ends_in.subset with endsE, edges), (endsE with a, aInE)⟩106    obtain ⟨C, closes, aInC, evenC⟩ :=107      SpanningTree.fundamental with finiteVertices, ends, tree, aNotT108    have growF : T ∪ G ⊆ T ∪ (G ∪ {a}) by simp109    have growC : T ∪ {a} ⊆ T ∪ (G ∪ {a}) by simp110    refine ⟨F △ C, (symmetricDifference.subset111      with (Subset.transitive with inside, growF),112        (Subset.transitive with closes, growC)),113      (EvenEdgeSet.symmetricDifference with even, evenC), _⟩114    intros g hg115    rw symmetricDifference.membership116    simp at hg117    rcases hg with inG | rfl118    . -- An edge of G lies in F, and outside C: it is neither in T nor a.119      have inF := covers with g, inG120      obtain ⟨_, gNotT⟩ :=121        difference.membership.forward with (GSubset with g, inG)122      have notA : g ≠ a123        intro same124        rw same at inG125        exact aFresh with inG126      have notC : ¬g ∈ C127        intro inC128        have inBig := closes with g, inC129        simp at inBig130      tauto131    . -- a lies in C, and outside F ⊆ T ∪ G.132      have notF : ¬a ∈ F133        intro inF134        have inBig := inside with a, inF135        simp at inBig136      tauto137138-- The even set of a spanning tree's complement: the symmetric difference of139-- the fundamental even sets of the edges outside the tree.140theorem SpanningTree.even_superset (V E leftEnd rightEnd T : Set)141  requires graph : Graph(V, E, leftEnd, rightEnd)142  requires finiteVertices : Finite(V)143  requires finiteEdges : Finite(E)144  requires tree : SpanningTree(V, leftEnd, rightEnd, T)145  requires edges : T ⊆ E146  shows ∃ F ⊆ E, EvenEdgeSet(V, leftEnd, rightEnd, F) ∧ E ∖ T ⊆ F147proof148  have outside := Subset.reflexive at E ∖ T149  have finite := Finite.difference at E, T with finiteEdges150  obtain ⟨F, inside, even, covers⟩ := SpanningTree.even_superset_of151    with graph, finiteVertices, finite, tree, edges, outside152  have whole : T ∪ (E ∖ T) ⊆ E by simp153  exact ⟨F, (Subset.transitive with inside, whole), even, covers⟩154155-- Section: Even covers from three spanning trees.156157-- Three spanning trees with no common edge give an even cover: the158-- complement of each tree lies in an even set, and every edge misses a tree.159theorem EvenCover.of_three_trees (V E leftEnd rightEnd T : Set)160  requires graph : Graph(V, E, leftEnd, rightEnd)161  requires finiteVertices : Finite(V)162  requires finiteEdges : Finite(E)163  requires trees : FunctionBetween(T, 3, 𝒫(E)) ∧164    (∀ i ∈ 3, SpanningTree(V, leftEnd, rightEnd, T(i)))165  requires sparse : T(0) ∩ T(1) ∩ T(2) = ∅166  shows ∃ F, EvenCover(V, E, leftEnd, rightEnd, F)167proof168  obtain ⟨function, spanning⟩ := trees169  have zero : 0 ∈ 3 by simp [membership.three]170  have one : 1 ∈ 3 by simp [membership.three]171  have two : 2 ∈ 3 by simp [membership.three]172  -- Each tree's complement lies in an even set.173  have superset : ∀ i ∈ 3, ∃ F ⊆ E,174      EvenEdgeSet(V, leftEnd, rightEnd, F) ∧ E ∖ T(i) ⊆ F175    intros i hi176    have edges : T(i) ⊆ E := powerset.membership_iff.forward177      with (FunctionBetween.apply_closed with function, hi)178    exact SpanningTree.even_superset179      with graph, finiteVertices, finiteEdges, (spanning with i, hi), edges180  obtain ⟨F0, in0, even0, cover0⟩ := superset with 0, zero181  obtain ⟨F1, in1, even1, cover1⟩ := superset with 1, one182  obtain ⟨F2, in2, even2, cover2⟩ := superset with 2, two183  have mem0 : F0 ∈ 𝒫(E) := powerset.membership_iff.backward with in0184  have mem1 : F1 ∈ 𝒫(E) := powerset.membership_iff.backward with in1185  have mem2 : F2 ∈ 𝒫(E) := powerset.membership_iff.backward with in2186  have values := tripleMap.value with mem0, mem1, mem2187  witness tripleMap(𝒫(E), F0, F1, F2)188  refine ⟨(tripleMap.function with mem0, mem1, mem2), _, _⟩189  . intros i hi190    have cases := membership.three.forward with hi191    rcases cases with rfl | rfl | rfl192    . rw values.left193      exact even0194    . rw values.right.left195      exact even1196    . rw values.right.right197      exact even2198  . -- An edge misses one of the three trees, so one even set holds it.199    intros e he200    have misses : e ∉ T(0) ∨ e ∉ T(1) ∨ e ∉ T(2)201      by_contra all202      have inAll : e ∈ T(0) ∧ e ∈ T(1) ∧ e ∈ T(2) by tauto203      have common : e ∈ T(0) ∩ T(1) ∩ T(2)204        by simp [inAll.left, inAll.right.left, inAll.right.right]205      rw sparse at common206      simp at common207    rcases misses with miss | miss | miss208    . refine ⟨0, zero, _⟩209      rw values.left210      exact cover0 with e, (difference.membership.backward with he, miss)211    . refine ⟨1, one, _⟩212      rw values.right.left213      exact cover1 with e, (difference.membership.backward with he, miss)214    . refine ⟨2, two, _⟩215      rw values.right.right216      exact cover2 with e, (difference.membership.backward with he, miss)217218theorem EvenCover.of_three_edge_connected (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 ∃ F, EvenCover(V, E, leftEnd, rightEnd, F)225proof226  obtain ⟨T, function, spanning, sparse⟩ := EdgeConnected.three_trees227    with graph, finiteVertices, finiteEdges, nonempty, connected228  exact EvenCover.of_three_trees229    with graph, finiteVertices, finiteEdges, ⟨function, spanning⟩, sparse230