Grace/Cumulus/GraphTheory/TreePacking/ExchangeOrder.g17

Open in Workbench Download source

Imports

Exchange

Declarations

Source

1-- The exchange improves the decomposition: the partition sequence and the2-- chosen colours agree with the original below the level of the exchanged3-- edge, and at that level the exchange is coarser or chooses a larger4-- colour, so it precedes the original in the order.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.TreePacking.ExchangeOrder11import Exchange1213-- Connectivity of a vertex set is monotone in the edge set, and survives14-- the replacement of an edge whose ends the new edges join.15theorem Connects.monotone (S leftEnd rightEnd F G : Set)16  requires subset : F ⊆ G17  requires connected : Connects(S, leftEnd, rightEnd, F)18  shows Connects(S, leftEnd, rightEnd, G)19proof20  intros u hu v hv21  exact Joined.monotone with subset, (connected with u, hu, v, hv)2223theorem Connects.replace_edge (V S leftEnd rightEnd F G g : Set)24  requires ends : ∀ h ∈ G, leftEnd(h) ∈ V ∧ rightEnd(h) ∈ V25  requires edgeEnds : leftEnd(g) ∈ V ∧ rightEnd(g) ∈ V26  requires cover : F ⊆ G ∪ {g}27  requires bridged : Joined(leftEnd, rightEnd, G, leftEnd(g), rightEnd(g))28  requires connected : Connects(S, leftEnd, rightEnd, F)29  shows Connects(S, leftEnd, rightEnd, G)30proof31  intros u hu v hv32  have joined := Joined.monotone with cover, (connected with u, hu, v, hv)33  exact Joined.drop_edge with ends, edgeEnds, joined, bridged3435-- A component of F within X is connected by the edges of F inside it.36theorem componentBy.connects_inside (X leftEnd rightEnd F u : Set)37  requires ends : ∀ e ∈ F, leftEnd(e) ∈ X ∧ rightEnd(e) ∈ X38  requires vertex : u ∈ X39  shows Connects(componentBy(X, leftEnd, rightEnd, F, u), leftEnd, rightEnd,40    inside(leftEnd, rightEnd, F, componentBy(X, leftEnd, rightEnd, F, u)))41proof42  have closed := componentBy.closed at X, leftEnd, rightEnd, F, u with ends43  intros v hv w hw44  obtain ⟨vIn, joinedV⟩ := hv45  obtain ⟨_, joinedW⟩ := hw46  have back := Joined.symmetric with ends, vertex, vIn, joinedV47  have joined := Joined.transitive with back, joinedW48  exact Joined.inside with closed, hv, joined4950-- In an even set whose edges all keep their ends within classes of P, the51-- ends of an edge inside the class S are joined by the other edges inside S.52theorem EvenEdgeSet.joined_inside (V P S leftEnd rightEnd C h : Set)53  requires finiteVertices : Finite(V)54  requires partition : Partition(V, P)55  requires class : S ∈ P56  requires ends : ∀ g ∈ C, leftEnd(g) ∈ V ∧ rightEnd(g) ∈ V57  requires even : EvenEdgeSet(V, leftEnd, rightEnd, C)58  requires edge : h ∈ C59  requires inside : leftEnd(h) ∈ S ∧ rightEnd(h) ∈ S60  requires together :61    ∀ g ∈ C, ∃ Y ∈ P, leftEnd(g) ∈ Y ∧ rightEnd(g) ∈ Y62  shows Joined(leftEnd, rightEnd, inside(leftEnd, rightEnd, C ∖ {h}, S),63    leftEnd(h), rightEnd(h))64proof65  have closed : ClosedUnder(leftEnd, rightEnd, C, S)66    intros g inC67    obtain ⟨Y, classY, leftY, rightY⟩ := together with g, inC68    by_cases same : S = Y69    . rw same70      tauto71    . have apartSY := Disjoint.iff.forward72        with (partition.right.left with S, class, Y, classY, same)73      constructor74      . intro leftS75        exfalso76        exact apartSY with leftEnd(g), leftS, leftY77      . intro rightS78        exfalso79        exact apartSY with rightEnd(g), rightS, rightY80  have joinedC := EvenEdgeSet.ends_joined with finiteVertices, ends, even, edge81  have restSubset := difference.subset_left at C, {h}82  have closedRest : ClosedUnder(leftEnd, rightEnd, C ∖ {h}, S)83    intros g inRest84    exact closed with g, (restSubset with g, inRest)85  exact Joined.inside with closedRest, inside.left, joinedC8687-- Replacing an edge h of F by an edge g keeps a vertex set S connected from88-- within when the ends of h, if both in S, stay joined inside S without h.89theorem Connects.inside_replace (V S leftEnd rightEnd F g h : Set)90  requires ends : ∀ x ∈ F ∪ {g}, leftEnd(x) ∈ V ∧ rightEnd(x) ∈ V91  requires edgeEnds : leftEnd(h) ∈ V ∧ rightEnd(h) ∈ V92  requires connected :93    Connects(S, leftEnd, rightEnd, inside(leftEnd, rightEnd, F, S))94  requires bridged : leftEnd(h) ∈ S ∧ rightEnd(h) ∈ S →95    Joined(leftEnd, rightEnd, inside(leftEnd, rightEnd, (F ∪ {g}) ∖ {h}, S),96      leftEnd(h), rightEnd(h))97  shows Connects(S, leftEnd, rightEnd,98    inside(leftEnd, rightEnd, (F ∪ {g}) ∖ {h}, S))99proof100  have endsSwapped := ends_in.subset with ends,101    (difference.subset_left at F ∪ {g}, {h})102  have endsInside := ends_in.subset with endsSwapped,103    (inside.subset at leftEnd, rightEnd, (F ∪ {g}) ∖ {h}, S)104  by_cases hInside : leftEnd(h) ∈ S ∧ rightEnd(h) ∈ S105  . have cover : inside(leftEnd, rightEnd, F, S) ⊆106        inside(leftEnd, rightEnd, (F ∪ {g}) ∖ {h}, S) ∪ {h}107      intros x inInside108      obtain ⟨inF, leftS, rightS⟩ := inInside109      by_cases same : x = h110      . rw same111        simp112      . have inSwapped : x ∈ (F ∪ {g}) ∖ {h} by simp [inF, same]113        have member : x ∈ inside(leftEnd, rightEnd, (F ∪ {g}) ∖ {h}, S) :=114          ⟨inSwapped, leftS, rightS⟩115        simp [member]116    exact Connects.replace_edge with117      endsInside, edgeEnds, cover, (bridged with hInside), connected118  . have subset : inside(leftEnd, rightEnd, F, S) ⊆119        inside(leftEnd, rightEnd, (F ∪ {g}) ∖ {h}, S)120      intros x inInside121      obtain ⟨inF, leftS, rightS⟩ := inInside122      have notH : x ≠ h123        intro same124        rw same at leftS, rightS125        exact hInside with ⟨leftS, rightS⟩126      refine ⟨?_, leftS, rightS⟩127      simp [inF, notH]128    exact Connects.monotone with subset, connected129130-- Claim 1 of the proof: a class S of a stage up to m + 1 that a colour131-- connects from within stays connected from within after the exchange.132-- Colour c loses f, whose ends, when both in S, are joined inside S by the133-- rest of the even set closed by e, since f has the least level there;134-- the last colour loses e, whose ends, when both in S, are joined inside S135-- by the rest of its even set, every edge of which has level at least m.136theorem exchange.transfer (V E leftEnd rightEnd T e f S : Set, c k m n i : Nat)137  requires graph : Graph(V, E, leftEnd, rightEnd)138  requires finiteVertices : Finite(V)139  requires nonempty : V ≠ ∅140  requires decomposition : Decomposition(E, T, succ(k))141  requires level : FiniteLevel(V, leftEnd, rightEnd, T, e, succ(k), m)142  requires least : ∀ g ∈ T(k), ∀ n ∈ ℕ,143    FiniteLevel(V, leftEnd, rightEnd, T, g, succ(k), n) →144    (∃ C, C ⊆ T(k) ∧ g ∈ C ∧ EvenEdgeSet(V, leftEnd, rightEnd, C)) →145      m ≤ n146  requires cycle :147    ∃ C, C ⊆ T(k) ∧ e ∈ C ∧ EvenEdgeSet(V, leftEnd, rightEnd, C)148  requires closes : ∃ C, C ⊆ T(c) ∪ {e} ∧ e ∈ C ∧ f ∈ C ∧149    f ≠ e ∧ EvenEdgeSet(V, leftEnd, rightEnd, C) ∧150    (∀ g ∈ C, ∀ n ∈ ℕ,151      FiniteLevel(V, leftEnd, rightEnd, T, g, succ(k), n) →152      (∃ p ∈ ℕ,153        FiniteLevel(V, leftEnd, rightEnd, T, f, succ(k), p) ∧ p ≤ n))154  requires colourC : c ∈ k155  requires first : e ∈ T(k)156  requires second : f ∈ T(c)157  requires bound : n ≤ succ(m)158  requires class : S ∈ partitionSequence(V, leftEnd, rightEnd, T, succ(k), n)159  requires index : i ∈ succ(k)160  requires connected :161    Connects(S, leftEnd, rightEnd, inside(leftEnd, rightEnd, T(i), S))162  shows Connects(S, leftEnd, rightEnd,163    inside(leftEnd, rightEnd, exchange(E, T, e, f, c, k)(i), S))164proof165  have partition :166      Partition(V, partitionSequence(V, leftEnd, rightEnd, T, succ(k), n)) :=167    partitionSequence.partition with graph, nonempty, decomposition168  have kIn : k ∈ succ(k) by simp169  have cIn : c ∈ succ(k) by simp [colourC]170  have endsK := Decomposition.ends with graph, decomposition, kIn171  have endsC := Decomposition.ends with graph, decomposition, cIn172  have endsE := endsK with e, first173  have endsF := endsC with f, second174  have mNatural : m ∈ ℕ := nat.omega.forward at m with *175  by_cases ic : i = c176  . rw [ic, (exchange.value_colour with decomposition, colourC, first, second)]177    rw ic at connected178    -- When the ends of f share S, n ≤ level(f), so every edge of the even179    -- set C closed by e keeps its ends in a class of stage n, and C ∖ {f}180    -- joins the ends of f inside S.181    have bridged : leftEnd(f) ∈ S ∧ rightEnd(f) ∈ S →182        Joined(leftEnd, rightEnd,183          inside(leftEnd, rightEnd, (T(c) ∪ {e}) ∖ {f}, S),184          leftEnd(f), rightEnd(f))185      intro fInside186      obtain ⟨C, subsetC, eInC, fInC, different, even, minimal⟩ := closes187      obtain ⟨p, pNatural, fLevel, _⟩ :=188        minimal with e, eInC, m, mNatural, level189      have pNat := nat.omega.backward with pNatural190      have nLe := FiniteLevel.le_of_together with191        graph, decomposition, fLevel, ⟨S, class, fInside⟩192      have endsCedges : ∀ g ∈ C, leftEnd(g) ∈ V ∧ rightEnd(g) ∈ V :=193        ends_in.subset with (ends_in.union_edge with endsC, endsE), subsetC194      have togetherAll : ∀ g ∈ C,195          ∃ Y ∈ partitionSequence(V, leftEnd, rightEnd, T, succ(k), n),196            leftEnd(g) ∈ Y ∧ rightEnd(g) ∈ Y197        intros g inC198        apply FiniteLevel.together_of_least with (endsCedges with g, inC)199        intros q qNatural gLevel200        obtain ⟨p₂, p₂Natural, fLevel₂, below⟩ :=201          minimal with g, inC, q, qNatural, gLevel202        have same :=203          FiniteLevel.unique with graph, decomposition, fLevel, fLevel₂204        have qNat := nat.omega.backward with qNatural205        rw ← same at below206        arith207      have joinedRest := EvenEdgeSet.joined_inside with finiteVertices,208        partition, class, endsCedges, even, fInC, fInside, togetherAll209      have restSubset : C ∖ {f} ⊆ (T(c) ∪ {e}) ∖ {f} :=210        difference.subset_of_subset with subsetC211      exact Joined.monotone with (inside.monotone with restSubset), joinedRest212    exact Connects.inside_replace with213      (ends_in.union_edge with endsC, endsE), endsF, connected, bridged214  by_cases ik : i = k215  . rw [ik, (exchange.value_last with decomposition, colourC, first, second)]216    rw ik at connected217    -- When the ends of e share S, n ≤ m, so every edge of the even set C₀218    -- of e keeps its ends in a class of stage n, and C₀ ∖ {e} joins the219    -- ends of e inside S.220    have bridged : leftEnd(e) ∈ S ∧ rightEnd(e) ∈ S →221        Joined(leftEnd, rightEnd,222          inside(leftEnd, rightEnd, (T(k) ∪ {f}) ∖ {e}, S),223          leftEnd(e), rightEnd(e))224      intro eInside225      obtain ⟨C₀, subsetC₀, eInC₀, even₀⟩ := cycle226      have nLe := FiniteLevel.le_of_together with227        graph, decomposition, level, ⟨S, class, eInside⟩228      have endsC₀ : ∀ g ∈ C₀, leftEnd(g) ∈ V ∧ rightEnd(g) ∈ V :=229        ends_in.subset with endsK, subsetC₀230      have togetherAll : ∀ g ∈ C₀,231          ∃ Y ∈ partitionSequence(V, leftEnd, rightEnd, T, succ(k), n),232            leftEnd(g) ∈ Y ∧ rightEnd(g) ∈ Y233        intros g inC₀234        apply FiniteLevel.together_of_least with (endsC₀ with g, inC₀)235        intros q qNatural gLevel236        have mLe := least with g, (subsetC₀ with g, inC₀), q, qNatural,237          gLevel, ⟨C₀, subsetC₀, inC₀, even₀⟩238        have qNat := nat.omega.backward with qNatural239        arith240      have joinedRest := EvenEdgeSet.joined_inside with finiteVertices,241        partition, class, endsC₀, even₀, eInC₀, eInside, togetherAll242      have restSubset : C₀ ∖ {e} ⊆ (T(k) ∪ {f}) ∖ {e} :=243        difference.subset_of_subset with244          (Subset.transitive with subsetC₀, union2.subset_left)245      exact Joined.monotone with (inside.monotone with restSubset), joinedRest246    exact Connects.inside_replace with247      (ends_in.union_edge with endsK, endsF), endsE, connected, bridged248  rw (exchange.value_other with249    decomposition, colourC, first, second, index, ic, ik)250  exact connected251252-- With equal partitions at a stage up to m + 1, the exchanged253-- decomposition chooses no smaller colour: a colour below the one chosen254-- for T is internally connected for T, hence for the exchange.255theorem exchange.colour_le (V E leftEnd rightEnd T e f : Set, c k m n : Nat)256  requires graph : Graph(V, E, leftEnd, rightEnd)257  requires finiteVertices : Finite(V)258  requires nonempty : V ≠ ∅259  requires decomposition : Decomposition(E, T, succ(k))260  requires level : FiniteLevel(V, leftEnd, rightEnd, T, e, succ(k), m)261  requires least : ∀ g ∈ T(k), ∀ n ∈ ℕ,262    FiniteLevel(V, leftEnd, rightEnd, T, g, succ(k), n) →263    (∃ C, C ⊆ T(k) ∧ g ∈ C ∧ EvenEdgeSet(V, leftEnd, rightEnd, C)) →264      m ≤ n265  requires cycle :266    ∃ C, C ⊆ T(k) ∧ e ∈ C ∧ EvenEdgeSet(V, leftEnd, rightEnd, C)267  requires closes : ∃ C, C ⊆ T(c) ∪ {e} ∧ e ∈ C ∧ f ∈ C ∧268    f ≠ e ∧ EvenEdgeSet(V, leftEnd, rightEnd, C) ∧269    (∀ g ∈ C, ∀ n ∈ ℕ,270      FiniteLevel(V, leftEnd, rightEnd, T, g, succ(k), n) →271      (∃ p ∈ ℕ,272        FiniteLevel(V, leftEnd, rightEnd, T, f, succ(k), p) ∧ p ≤ n))273  requires colourC : c ∈ k274  requires first : e ∈ T(k)275  requires second : f ∈ T(c)276  requires bound : n ≤ succ(m)277  requires same : partitionSequence(V, leftEnd, rightEnd, T, succ(k), n) =278    partitionSequence(V, leftEnd, rightEnd, exchange(E, T, e, f, c, k),279      succ(k), n)280  shows stageColour(leftEnd, rightEnd, T,281      partitionSequence(V, leftEnd, rightEnd, T, succ(k), n), succ(k)) ≤282    stageColour(leftEnd, rightEnd, exchange(E, T, e, f, c, k),283      partitionSequence(V, leftEnd, rightEnd, exchange(E, T, e, f, c, k),284        succ(k), n), succ(k))285proof286  have naturalT := stageColour.natural at leftEnd, rightEnd, T,287    partitionSequence(V, leftEnd, rightEnd, T, succ(k), n), succ(k)288  obtain ⟨b, colourB⟩ := exists_eq at stageColour(leftEnd, rightEnd,289    exchange(E, T, e, f, c, k), partitionSequence(V, leftEnd, rightEnd,290      exchange(E, T, e, f, c, k), succ(k), n), succ(k))291  have naturalB := stageColour.natural at leftEnd, rightEnd,292    exchange(E, T, e, f, c, k), partitionSequence(V, leftEnd, rightEnd,293      exchange(E, T, e, f, c, k), succ(k), n), succ(k)294  have memberB := stageColour.member at leftEnd, rightEnd,295    exchange(E, T, e, f, c, k), partitionSequence(V, leftEnd, rightEnd,296      exchange(E, T, e, f, c, k), succ(k), n), succ(k)297  rw ← colourB at naturalB, memberB298  rw ← colourB299  by_contra above300  have less := Less.of_not_LessEqual with above301  simp at memberB302  rcases memberB with inColours | isEnd303  . -- b is disconnected for the exchange but, being below the chosen304    -- colour of T, connected for T, so connected for the exchange.305    obtain ⟨bIn, bDisconnected⟩ := inColours306    have internalT : InternallyConnected(leftEnd, rightEnd, T(b),307        partitionSequence(V, leftEnd, rightEnd, T, succ(k), n))308      by_contra disconnected309      have inT : b ∈ disconnectedColour(leftEnd, rightEnd, T,310          partitionSequence(V, leftEnd, rightEnd, T, succ(k), n), succ(k)) ∪311          {succ(k)} by simp [bIn, disconnected]312      have below := stageColour.least with inT313      arith314    have internalU : InternallyConnected(leftEnd, rightEnd,315        exchange(E, T, e, f, c, k)(b),316        partitionSequence(V, leftEnd, rightEnd, T, succ(k), n))317      intros S classS318      exact exchange.transfer with graph, finiteVertices, nonempty,319        decomposition, level, least, cycle, closes, colourC, first, second,320        bound, classS, bIn, (internalT with S, classS)321    rw ← same at bDisconnected322    exact bDisconnected with internalU323  . have endIn : succ(k) ∈ disconnectedColour(leftEnd, rightEnd, T,324        partitionSequence(V, leftEnd, rightEnd, T, succ(k), n), succ(k)) ∪325        {succ(k)} by simp326    have below := stageColour.least with endIn327    rw isEnd at less328    arith329330-- With equal partitions and chosen colours at a moving stage n, the next331-- partitions of T and of the exchange refine P_n along T(c_n) and along332-- exchange(c_n).333theorem exchange.next_classes (V E leftEnd rightEnd T e f : Set, c k n : Nat)334  requires graph : Graph(V, E, leftEnd, rightEnd)335  requires nonempty : V ≠ ∅336  requires decomposition : Decomposition(E, T, succ(k))337  requires colourC : c ∈ k338  requires first : e ∈ T(k)339  requires second : f ∈ T(c)340  requires same : partitionSequence(V, leftEnd, rightEnd, T, succ(k), n) =341    partitionSequence(V, leftEnd, rightEnd, exchange(E, T, e, f, c, k),342      succ(k), n)343  requires colours : stageColour(leftEnd, rightEnd, T,344      partitionSequence(V, leftEnd, rightEnd, T, succ(k), n), succ(k)) =345    stageColour(leftEnd, rightEnd, exchange(E, T, e, f, c, k),346      partitionSequence(V, leftEnd, rightEnd, exchange(E, T, e, f, c, k),347        succ(k), n), succ(k))348  requires active : disconnectedColour(leftEnd, rightEnd, T,349    partitionSequence(V, leftEnd, rightEnd, T, succ(k), n), succ(k)) ≠ ∅350  shows partitionSequence(V, leftEnd, rightEnd, T, succ(k), succ(n)) =351      refineBy(leftEnd, rightEnd, T(leastNatural(disconnectedColour(leftEnd,352        rightEnd, T, partitionSequence(V, leftEnd, rightEnd, T, succ(k), n),353        succ(k)))), partitionSequence(V, leftEnd, rightEnd, T, succ(k), n)) ∧354    partitionSequence(V, leftEnd, rightEnd, exchange(E, T, e, f, c, k),355        succ(k), succ(n)) =356      refineBy(leftEnd, rightEnd, exchange(E, T, e, f, c, k)(leastNatural(357        disconnectedColour(leftEnd, rightEnd, T,358          partitionSequence(V, leftEnd, rightEnd, T, succ(k), n), succ(k)))),359        partitionSequence(V, leftEnd, rightEnd, T, succ(k), n))360proof361  have partition :362      Partition(V, partitionSequence(V, leftEnd, rightEnd, T, succ(k), n)) :=363    partitionSequence.partition with graph, nonempty, decomposition364  obtain ⟨colourIn, _⟩ := disconnectedColour.least with active365  have ends := Decomposition.ends with graph, decomposition, colourIn366  have decompositionU := exchange.decomposition367    at V, E, leftEnd, rightEnd, T, e, f, c, k368    with decomposition, colourC, first, second369  have endsU := Decomposition.ends with graph, decompositionU, colourIn370  have stageT := stageColour.of_some with active371  rw [stageT, ← same] at colours372  have activeU : disconnectedColour(leftEnd, rightEnd,373      exchange(E, T, e, f, c, k),374      partitionSequence(V, leftEnd, rightEnd, T, succ(k), n), succ(k)) ≠ ∅375    intro none376    rw (stageColour.of_none with none) at colours377    rw colours at colourIn378    exact membership.irreflexive with colourIn379  have stageU := stageColour.of_some with activeU380  rw stageU at colours381  rw under colours at endsU382  constructor383  . rw [partitionSequence.succ,384      (partitionStep.refined with partition, ends, active)]385  . rw [partitionSequence.succ, ← same,386      (partitionStep.refined with partition, endsU, activeU), ← colours]387388-- Claim 2, the partition half: under agreement at a moving stage n ≤ m the389-- next partition of T refines that of the exchange, as each class of the390-- former, connected from within by T(c_n), is connected from within by391-- exchange(c_n) and so lies in a class of the latter.392theorem exchange.refines_next (V E leftEnd rightEnd T e f : Set, c k m n : Nat)393  requires graph : Graph(V, E, leftEnd, rightEnd)394  requires finiteVertices : Finite(V)395  requires nonempty : V ≠ ∅396  requires decomposition : Decomposition(E, T, succ(k))397  requires level : FiniteLevel(V, leftEnd, rightEnd, T, e, succ(k), m)398  requires least : ∀ g ∈ T(k), ∀ n ∈ ℕ,399    FiniteLevel(V, leftEnd, rightEnd, T, g, succ(k), n) →400    (∃ C, C ⊆ T(k) ∧ g ∈ C ∧ EvenEdgeSet(V, leftEnd, rightEnd, C)) →401      m ≤ n402  requires cycle :403    ∃ C, C ⊆ T(k) ∧ e ∈ C ∧ EvenEdgeSet(V, leftEnd, rightEnd, C)404  requires closes : ∃ C, C ⊆ T(c) ∪ {e} ∧ e ∈ C ∧ f ∈ C ∧405    f ≠ e ∧ EvenEdgeSet(V, leftEnd, rightEnd, C) ∧406    (∀ g ∈ C, ∀ n ∈ ℕ,407      FiniteLevel(V, leftEnd, rightEnd, T, g, succ(k), n) →408      (∃ p ∈ ℕ,409        FiniteLevel(V, leftEnd, rightEnd, T, f, succ(k), p) ∧ p ≤ n))410  requires colourC : c ∈ k411  requires first : e ∈ T(k)412  requires second : f ∈ T(c)413  requires bound : n ≤ m414  requires same : partitionSequence(V, leftEnd, rightEnd, T, succ(k), n) =415    partitionSequence(V, leftEnd, rightEnd, exchange(E, T, e, f, c, k),416      succ(k), n)417  requires colours : stageColour(leftEnd, rightEnd, T,418      partitionSequence(V, leftEnd, rightEnd, T, succ(k), n), succ(k)) =419    stageColour(leftEnd, rightEnd, exchange(E, T, e, f, c, k),420      partitionSequence(V, leftEnd, rightEnd, exchange(E, T, e, f, c, k),421        succ(k), n), succ(k))422  requires active : disconnectedColour(leftEnd, rightEnd, T,423    partitionSequence(V, leftEnd, rightEnd, T, succ(k), n), succ(k)) ≠ ∅424  shows Refines(partitionSequence(V, leftEnd, rightEnd, T, succ(k), succ(n)),425    partitionSequence(V, leftEnd, rightEnd, exchange(E, T, e, f, c, k),426      succ(k), succ(n)))427proof428  obtain ⟨nextT, nextU⟩ := exchange.next_classes with graph, nonempty,429    decomposition, colourC, first, second, same, colours, active430  obtain ⟨colourIn, _⟩ := disconnectedColour.least with active431  obtain ⟨d, colourD⟩ := exists_eq at leastNatural(disconnectedColour(432    leftEnd, rightEnd, T,433    partitionSequence(V, leftEnd, rightEnd, T, succ(k), n), succ(k)))434  rw ← colourD at nextT, nextU, colourIn435  have dNat := natural.member at succ(k) with d, colourIn436  have boundSucc : succ(n) ≤ succ(m) by arith437  intros S classS438  have classNext := classS439  rw nextT at classS440  obtain ⟨X, classX, inComponents⟩ :=441    refineBy.membership.forward with classS442  obtain ⟨u, uIn, rfl⟩ := inComponents443  have endsX := inside.ends at leftEnd, rightEnd, T(d), X444  have connectedS := componentBy.connects_inside with endsX, uIn445  have connectedT := Connects.monotone with446    (inside.monotone with (inside.subset at leftEnd, rightEnd, T(d), X)),447    connectedS448  have connectedU := exchange.transfer with graph, finiteVertices, nonempty,449    decomposition, level, least, cycle, closes, colourC, first, second,450    boundSucc, classNext, colourIn, connectedT451  have selfU := componentBy.self452    at X, leftEnd, rightEnd, inside(leftEnd, rightEnd, T(d), X), u with uIn453  have subsetX := componentBy.subset454    at X, leftEnd, rightEnd, inside(leftEnd, rightEnd, T(d), X), u455  have grow : inside(leftEnd, rightEnd, exchange(E, T, e, f, c, k)(d),456      componentBy(X, leftEnd, rightEnd, inside(leftEnd, rightEnd, T(d), X), u))457      ⊆ inside(leftEnd, rightEnd, exchange(E, T, e, f, c, k)(d), X)458    intros g inInside459    obtain ⟨inU, leftS, rightS⟩ := inInside460    exact ⟨inU, (subsetX with leftEnd(g), leftS),461      (subsetX with rightEnd(g), rightS)⟩462  witness componentBy(X, leftEnd, rightEnd,463    inside(leftEnd, rightEnd, exchange(E, T, e, f, c, k)(d), X), u)464  rw nextU465  refine ⟨?_, ?_⟩466  . exact refineBy.membership.backward with467      ⟨X, classX, (componentsBy.contains with uIn)⟩468  . intros v hv469    have joined := connectedU with u, selfU, v, hv470    exact ⟨(subsetX with v, hv), (Joined.monotone with grow, joined)⟩471472-- At a stage n ≤ m + 1 where the partitions agree, and the earlier stages473-- agree, the exchange chooses no smaller colour: either it chooses a larger474-- one, and T precedes it at stage n, or the agreement reaches stage n.475theorem exchange.agree_step (V E leftEnd rightEnd T e f : Set, c k m n : Nat)476  requires graph : Graph(V, E, leftEnd, rightEnd)477  requires finiteVertices : Finite(V)478  requires nonempty : V ≠ ∅479  requires decomposition : Decomposition(E, T, succ(k))480  requires level : FiniteLevel(V, leftEnd, rightEnd, T, e, succ(k), m)481  requires least : ∀ g ∈ T(k), ∀ n ∈ ℕ,482    FiniteLevel(V, leftEnd, rightEnd, T, g, succ(k), n) →483    (∃ C, C ⊆ T(k) ∧ g ∈ C ∧ EvenEdgeSet(V, leftEnd, rightEnd, C)) →484      m ≤ n485  requires cycle :486    ∃ C, C ⊆ T(k) ∧ e ∈ C ∧ EvenEdgeSet(V, leftEnd, rightEnd, C)487  requires closes : ∃ C, C ⊆ T(c) ∪ {e} ∧ e ∈ C ∧ f ∈ C ∧488    f ≠ e ∧ EvenEdgeSet(V, leftEnd, rightEnd, C) ∧489    (∀ g ∈ C, ∀ n ∈ ℕ,490      FiniteLevel(V, leftEnd, rightEnd, T, g, succ(k), n) →491      (∃ p ∈ ℕ,492        FiniteLevel(V, leftEnd, rightEnd, T, f, succ(k), p) ∧ p ≤ n))493  requires colourC : c ∈ k494  requires first : e ∈ T(k)495  requires second : f ∈ T(c)496  requires bound : n ≤ succ(m)497  requires same : partitionSequence(V, leftEnd, rightEnd, T, succ(k), n) =498    partitionSequence(V, leftEnd, rightEnd, exchange(E, T, e, f, c, k),499      succ(k), n)500  requires agree : ∀ i ∈ n,501      partitionSequence(V, leftEnd, rightEnd, T, succ(k), i) =502        partitionSequence(V, leftEnd, rightEnd, exchange(E, T, e, f, c, k),503          succ(k), i) ∧504      stageColour(leftEnd, rightEnd, T,505          partitionSequence(V, leftEnd, rightEnd, T, succ(k), i), succ(k)) =506        stageColour(leftEnd, rightEnd, exchange(E, T, e, f, c, k),507          partitionSequence(V, leftEnd, rightEnd, exchange(E, T, e, f, c, k),508            succ(k), i), succ(k))509  shows Precedes(V, leftEnd, rightEnd, T, exchange(E, T, e, f, c, k),510      succ(k)) ∨511    (∀ i ∈ succ(n),512      partitionSequence(V, leftEnd, rightEnd, T, succ(k), i) =513        partitionSequence(V, leftEnd, rightEnd, exchange(E, T, e, f, c, k),514          succ(k), i) ∧515      stageColour(leftEnd, rightEnd, T,516          partitionSequence(V, leftEnd, rightEnd, T, succ(k), i), succ(k)) =517        stageColour(leftEnd, rightEnd, exchange(E, T, e, f, c, k),518          partitionSequence(V, leftEnd, rightEnd, exchange(E, T, e, f, c, k),519            succ(k), i), succ(k)))520proof521  have below := exchange.colour_le with graph, finiteVertices, nonempty,522    decomposition, level, least, cycle, closes, colourC, first, second,523    bound, same524  have naturalT := stageColour.natural at leftEnd, rightEnd, T,525    partitionSequence(V, leftEnd, rightEnd, T, succ(k), n), succ(k)526  have naturalU := stageColour.natural at leftEnd, rightEnd,527    exchange(E, T, e, f, c, k), partitionSequence(V, leftEnd, rightEnd,528      exchange(E, T, e, f, c, k), succ(k), n), succ(k)529  have natural : n ∈ ℕ := nat.omega.forward at n with *530  have order := LessEqual.cases with below531  rcases order with less | equal532  . left533    refine ⟨n, natural, agree, ?_⟩534    right535    exact ⟨same, less⟩536  . right537    intros i member538    have cases := membership.successor_forward{n := n} with member539    rcases cases with earlier | isN540    . exact agree with i, earlier541    . rw isN542      exact ⟨same, equal⟩543544-- Claim 2: up to stage m, either the exchange already precedes T at some545-- stage, or the partitions and chosen colours agree at every stage so far.546theorem exchange.good_below (V E leftEnd rightEnd T e f : Set, c k m n : Nat)547  requires graph : Graph(V, E, leftEnd, rightEnd)548  requires finiteVertices : Finite(V)549  requires nonempty : V ≠ ∅550  requires decomposition : Decomposition(E, T, succ(k))551  requires level : FiniteLevel(V, leftEnd, rightEnd, T, e, succ(k), m)552  requires least : ∀ g ∈ T(k), ∀ n ∈ ℕ,553    FiniteLevel(V, leftEnd, rightEnd, T, g, succ(k), n) →554    (∃ C, C ⊆ T(k) ∧ g ∈ C ∧ EvenEdgeSet(V, leftEnd, rightEnd, C)) →555      m ≤ n556  requires cycle :557    ∃ C, C ⊆ T(k) ∧ e ∈ C ∧ EvenEdgeSet(V, leftEnd, rightEnd, C)558  requires closes : ∃ C, C ⊆ T(c) ∪ {e} ∧ e ∈ C ∧ f ∈ C ∧559    f ≠ e ∧ EvenEdgeSet(V, leftEnd, rightEnd, C) ∧560    (∀ g ∈ C, ∀ n ∈ ℕ,561      FiniteLevel(V, leftEnd, rightEnd, T, g, succ(k), n) →562      (∃ p ∈ ℕ,563        FiniteLevel(V, leftEnd, rightEnd, T, f, succ(k), p) ∧ p ≤ n))564  requires colourC : c ∈ k565  requires first : e ∈ T(k)566  requires second : f ∈ T(c)567  requires some : disconnectedColour(leftEnd, rightEnd, T,568    partitionSequence(V, leftEnd, rightEnd, T, succ(k), m), succ(k)) ≠ ∅569  requires bound : n ≤ m570  shows Precedes(V, leftEnd, rightEnd, T, exchange(E, T, e, f, c, k),571      succ(k)) ∨572    (∀ i ∈ succ(n),573      partitionSequence(V, leftEnd, rightEnd, T, succ(k), i) =574        partitionSequence(V, leftEnd, rightEnd, exchange(E, T, e, f, c, k),575          succ(k), i) ∧576      stageColour(leftEnd, rightEnd, T,577          partitionSequence(V, leftEnd, rightEnd, T, succ(k), i), succ(k)) =578        stageColour(leftEnd, rightEnd, exchange(E, T, e, f, c, k),579          partitionSequence(V, leftEnd, rightEnd, exchange(E, T, e, f, c, k),580            succ(k), i), succ(k)))581proof582  induction n583  | zero =>584    intro bound585    have zeroT := partitionSequence.zero at V, leftEnd, rightEnd, T, succ(k)586    have zeroU := partitionSequence.zero587      at V, leftEnd, rightEnd, exchange(E, T, e, f, c, k), succ(k)588    have sameZero : partitionSequence(V, leftEnd, rightEnd, T, succ(k), 0) =589        partitionSequence(V, leftEnd, rightEnd, exchange(E, T, e, f, c, k),590          succ(k), 0)591      rw [zeroT, zeroU]592    have start : 0 ≤ succ(m) by arith593    have none : ∀ i ∈ 0,594        partitionSequence(V, leftEnd, rightEnd, T, succ(k), i) =595          partitionSequence(V, leftEnd, rightEnd, exchange(E, T, e, f, c, k),596            succ(k), i) ∧597        stageColour(leftEnd, rightEnd, T,598            partitionSequence(V, leftEnd, rightEnd, T, succ(k), i), succ(k)) =599          stageColour(leftEnd, rightEnd, exchange(E, T, e, f, c, k),600            partitionSequence(V, leftEnd, rightEnd,601              exchange(E, T, e, f, c, k), succ(k), i), succ(k))602      intros i member603      exfalso604      rw nat.zero at member605      exact set.empty with member606    exact exchange.agree_step with graph, finiteVertices, nonempty,607      decomposition, level, least, cycle, closes, colourC, first, second,608      start, sameZero, none609  | succ(q) using ih =>610    intro bound611    have earlier : q ≤ m by arith612    have result := ih with earlier613    rcases result with precedes | good614    . left615      exact precedes616    . have self : q ∈ succ(q) by simp617      obtain ⟨sameN, coloursN⟩ := good with q, self618      -- The sequence of T is still moving at stage q, as it moves at m.619      have active : disconnectedColour(leftEnd, rightEnd, T,620          partitionSequence(V, leftEnd, rightEnd, T, succ(k), q),621          succ(k)) ≠ ∅622        obtain ⟨d, dNat, sum⟩ := earlier623        rw ← sum at some624        exact partitionSequence.active with625          graph, nonempty, decomposition, some626      have refines := exchange.refines_next with graph, finiteVertices,627        nonempty, decomposition, level, least, cycle, closes, colourC, first,628        second, earlier, sameN, coloursN, active629      by_cases equal :630        partitionSequence(V, leftEnd, rightEnd, T, succ(k), succ(q)) =631          partitionSequence(V, leftEnd, rightEnd, exchange(E, T, e, f, c, k),632            succ(k), succ(q))633      . have boundSucc : succ(q) ≤ succ(m) by arith634        exact exchange.agree_step with graph, finiteVertices,635          nonempty, decomposition, level, least, cycle, closes, colourC,636          first, second, boundSucc, equal, good637      . left638        have natural : succ(q) ∈ ℕ := nat.omega.forward at succ(q) with *639        refine ⟨succ(q), natural, good, ?_⟩640        left641        exact ⟨refines, equal⟩642643-- Claims 1 and 2 of the proof, as the exchange step improving the644-- decomposition in the order.645theorem exchange.precedes (V E leftEnd rightEnd T e f : Set, c k m : Nat)646  requires graph : Graph(V, E, leftEnd, rightEnd)647  requires finiteVertices : Finite(V)648  requires finiteEdges : Finite(E)649  requires nonempty : V ≠ ∅650  requires decomposition : Decomposition(E, T, succ(k))651  requires trees : ∀ i ∈ k, SpanningTree(V, leftEnd, rightEnd, T(i))652  requires level : FiniteLevel(V, leftEnd, rightEnd, T, e, succ(k), m)653  requires least : ∀ g ∈ T(k), ∀ n ∈ ℕ,654    FiniteLevel(V, leftEnd, rightEnd, T, g, succ(k), n) →655    (∃ C, C ⊆ T(k) ∧ g ∈ C ∧ EvenEdgeSet(V, leftEnd, rightEnd, C)) →656      m ≤ n657  requires cycle :658    ∃ C, C ⊆ T(k) ∧ e ∈ C ∧ EvenEdgeSet(V, leftEnd, rightEnd, C)659  requires colour : c = leastNatural(disconnectedColour(leftEnd, rightEnd, T,660    partitionSequence(V, leftEnd, rightEnd, T, succ(k), m), succ(k)))661  requires closes : ∃ C, C ⊆ T(c) ∪ {e} ∧ e ∈ C ∧ f ∈ C ∧662    f ≠ e ∧ EvenEdgeSet(V, leftEnd, rightEnd, C) ∧663    (∀ g ∈ C, ∀ n ∈ ℕ,664      FiniteLevel(V, leftEnd, rightEnd, T, g, succ(k), n) →665      (∃ p ∈ ℕ,666        FiniteLevel(V, leftEnd, rightEnd, T, f, succ(k), p) ∧ p ≤ n))667  shows Precedes(V, leftEnd, rightEnd, T, exchange(E, T, e, f, c, k),668      succ(k)) ∧669    (∀ i ∈ k,670      SpanningTree(V, leftEnd, rightEnd, exchange(E, T, e, f, c, k)(i)))671proof672  -- The setting: e is of the last colour, c is a colour below k, and f is673  -- of colour c, as e is not.674  obtain ⟨C₀, subsetC₀, eInC₀, _⟩ := cycle675  have first : e ∈ T(k) := subsetC₀ with e, eInC₀676  obtain ⟨colourC, outside, some⟩ := FiniteLevel.colour_below with677    graph, nonempty, decomposition, level, first, colour678  have colourIn : c ∈ succ(k) by simp [colourC]679  obtain ⟨C, subsetC, eInC, fInC, different, even, _⟩ := closes680  have second : f ∈ T(c)681    have inUnion := subsetC with f, fInC682    simp [different] at inUnion683    exact inUnion684  refine ⟨?_, ?_⟩685  . -- Claim 2 up to stage m; then at m + 1 the partition of T refines686    -- that of the exchange and differs from it, since e, now of colour c,687    -- keeps its ends together there while T parts them.688    have selfM : m ≤ m := LessEqual.reflexive at m689    have result := exchange.good_below with graph, finiteVertices, nonempty,690      decomposition, level, least, cycle, closes, colourC, first, second,691      some, selfM692    rcases result with precedes | good693    . exact precedes694    . have selfIn : m ∈ succ(m) by simp695      obtain ⟨sameM, coloursM⟩ := good with m, selfIn696      obtain ⟨_, nextU⟩ := exchange.next_classes with graph, nonempty,697        decomposition, colourC, first, second, sameM, coloursM, some698      rw ← colour at nextU699      have refines := exchange.refines_next with graph, finiteVertices,700        nonempty, decomposition, level, least, cycle, closes, colourC, first,701        second, selfM, sameM, coloursM, some702      have eInU : e ∈ exchange(E, T, e, f, c, k)(c)703        rw exchange.class_membership with704          decomposition, colourC, first, second, colourIn705        left706        exact ⟨rfl, rfl⟩707      have strict :708          partitionSequence(V, leftEnd, rightEnd, T, succ(k), succ(m)) ≠709            partitionSequence(V, leftEnd, rightEnd, exchange(E, T, e, f, c, k),710              succ(k), succ(m))711        intro equal712        obtain ⟨together, parted⟩ := level713        obtain ⟨X, classX, leftIn, rightIn⟩ := together714        have insideEdge : e ∈ inside(leftEnd, rightEnd,715            exchange(E, T, e, f, c, k)(c), X) := ⟨eInU, leftIn, rightIn⟩716        have joined := Joined.of_edge at leftEnd, rightEnd, _, _ with insideEdge717        apply parted718        rw under equal719        rw under nextU720        exact refineBy.together with classX, ⟨leftIn, rightIn⟩, joined721      have natural : succ(m) ∈ ℕ := nat.omega.forward at succ(m) with *722      refine ⟨succ(m), natural, good, ?_⟩723      left724      exact ⟨refines, strict⟩725  . -- The trees: colour c exchanges f for e along the even set it closes,726    -- and the other colours below k are unchanged.727    intros i index728    have iNat := natural.member at k with i, index729    have inSucc : i ∈ succ(k) by simp [index]730    have less := Less.of_membership at i, k with index731    have notK : i ≠ k by arith732    by_cases ic : i = c733    . rw [ic, (exchange.value_colour with734        decomposition, colourC, first, second)]735      have kIn : k ∈ succ(k) by simp736      have endsC := Decomposition.ends with graph, decomposition, colourIn737      have endsK := Decomposition.ends with graph, decomposition, kIn738      have exchanged := SpanningTree.exchange with finiteVertices,739        ⟨endsC, (endsK with e, first)⟩, (trees with c, colourC), outside,740        even, ⟨subsetC, eInC⟩, ⟨fInC, different⟩741      have same : (T(c) ∪ {e}) ∖ {f} = (T(c) ∖ {f}) ∪ {e}742        ext g743        simp [different]744      rw same745      exact exchanged746    . rw (exchange.value_other with747        decomposition, colourC, first, second, inSucc, ic, notK)748      exact trees with i, index749