Grace/Cumulus/GraphTheory/TreePacking/Levels.g17

Open in Workbench Download source

Imports

Sequences

Declarations

Source

1-- The level of an edge in the partition sequence of a decomposition: the2-- last stage at which both ends share a class, finite exactly when the ends3-- part at some stage, together with the colour refined at that stage.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.Levels10import Sequences1112-- The level of an edge: the largest n at which both ends share a class of13-- P_n; an edge inside a class of the stable partition has infinite level.14predicate FiniteLevel (V leftEnd rightEnd T e : Set, k n : Nat) :=15  (∃ X ∈ partitionSequence(V, leftEnd, rightEnd, T, k, n),16    leftEnd(e) ∈ X ∧ rightEnd(e) ∈ X) ∧17  ¬(∃ X ∈ partitionSequence(V, leftEnd, rightEnd, T, k, succ(n)),18    leftEnd(e) ∈ X ∧ rightEnd(e) ∈ X)1920-- At stage 0 the ends of an edge share the one class V.21theorem partitionSequence.together_zero (V leftEnd rightEnd T e : Set, k : Nat)22  requires ends : leftEnd(e) ∈ V ∧ rightEnd(e) ∈ V23  shows ∃ X ∈ partitionSequence(V, leftEnd, rightEnd, T, k, 0),24    leftEnd(e) ∈ X ∧ rightEnd(e) ∈ X25proof26  witness V27  rw partitionSequence.zero28  exact ⟨singleton.self, ends.left, ends.right⟩2930-- An edge whose ends share a class at stage 0 but not at stage N has a31-- finite level below N: the last stage at which they still share one.32theorem FiniteLevel.of_parted (V leftEnd rightEnd T e : Set, k N : Nat)33  requires together :34    ∃ X ∈ partitionSequence(V, leftEnd, rightEnd, T, k, 0),35      leftEnd(e) ∈ X ∧ rightEnd(e) ∈ X36  requires parted :37    ¬(∃ X ∈ partitionSequence(V, leftEnd, rightEnd, T, k, N),38      leftEnd(e) ∈ X ∧ rightEnd(e) ∈ X)39  shows ∃ n ∈ ℕ, n < N ∧ FiniteLevel(V, leftEnd, rightEnd, T, e, k, n)40proof41  induction N42  | zero =>43    intro parted44    exfalso45    exact parted with together46  | succ(m) using ih =>47    intro parted48    by_cases shared :49      ∃ X ∈ partitionSequence(V, leftEnd, rightEnd, T, k, m),50        leftEnd(e) ∈ X ∧ rightEnd(e) ∈ X51    . witness m52      refine ⟨?_, ?_, ?_⟩53      . exact nat.omega.forward at m with *54      . arith55      . unfold FiniteLevel56        constructor57        . exact shared58        . exact parted59    . obtain ⟨n, natural, less, level⟩ := ih with shared60      have nNat := nat.omega.backward with natural61      refine ⟨n, natural, ?_, level⟩62      arith6364-- An edge crossing the stable partition has a finite level: its ends share65-- the class V at stage 0 and no class at stage |V|.66theorem FiniteLevel.of_crossing (V leftEnd rightEnd T F e : Set, k : Nat)67  requires finiteVertices : Finite(V)68  requires partition : Partition(V, stablePartition(V, leftEnd, rightEnd, T, k))69  requires ends : leftEnd(e) ∈ V ∧ rightEnd(e) ∈ V70  requires crossing : e ∈ crossingClasses(71    stablePartition(V, leftEnd, rightEnd, T, k), leftEnd, rightEnd, F)72  shows ∃ n ∈ ℕ, n < cardinality(V) ∧73    FiniteLevel(V, leftEnd, rightEnd, T, e, k, n)74proof75  unfold stablePartition at partition, crossing76  have together := partitionSequence.together_zero77    at V, leftEnd, rightEnd, T, e, k with ends78  have parted : ¬(∃ X ∈79      partitionSequence(V, leftEnd, rightEnd, T, k, cardinality(V)),80      leftEnd(e) ∈ X ∧ rightEnd(e) ∈ X)81    intro common82    have same := (classOf.eq_iff with partition, ends.left, ends.right).backward83      with common84    exact crossing.right with same85  exact FiniteLevel.of_parted with together, parted8687-- Ends sharing a class at a later stage share one at every earlier stage,88-- since the sequence refines; so an edge has one finite level.89theorem partitionSequence.earlier (V E leftEnd rightEnd T e : Set, k i d : Nat)90  requires graph : Graph(V, E, leftEnd, rightEnd)91  requires decomposition : Decomposition(E, T, k)92  requires together :93    ∃ X ∈ partitionSequence(V, leftEnd, rightEnd, T, k, i + d),94      leftEnd(e) ∈ X ∧ rightEnd(e) ∈ X95  shows ∃ X ∈ partitionSequence(V, leftEnd, rightEnd, T, k, i),96    leftEnd(e) ∈ X ∧ rightEnd(e) ∈ X97proof98  induction d99  | zero =>100    intro together101    rw under add.right_unit at together102    exact together103  | succ(n) using ih =>104    intro together105    apply ih106    rw under add.succ_right at together107    obtain ⟨X, class, leftIn, rightIn⟩ := together108    have refines := partitionSequence.refines109      at V, E, leftEnd, rightEnd, T, k, i + n with graph, decomposition110    obtain ⟨Y, classY, subset⟩ := refines with X, class111    exact ⟨Y, classY, (subset with leftEnd(e), leftIn),112      (subset with rightEnd(e), rightIn)⟩113114theorem FiniteLevel.unique (V E leftEnd rightEnd T e : Set, k m n : Nat)115  requires graph : Graph(V, E, leftEnd, rightEnd)116  requires decomposition : Decomposition(E, T, k)117  requires levelM : FiniteLevel(V, leftEnd, rightEnd, T, e, k, m)118  requires levelN : FiniteLevel(V, leftEnd, rightEnd, T, e, k, n)119  shows m = n120proof121  have order := Less.trichotomy at m, n with *122  rcases order with before | same | after123  . obtain ⟨d, dNat, sum⟩ := before124    have together := levelN.left125    rw under ← sum at together126    exfalso127    exact levelM.right with (partitionSequence.earlier with128      graph, decomposition, together)129  . exact same130  . obtain ⟨d, dNat, sum⟩ := after131    have together := levelM.left132    rw under ← sum at together133    exfalso134    exact levelN.right with (partitionSequence.earlier with135      graph, decomposition, together)136137-- An edge whose every finite level is at least n keeps its ends together138-- at stage n; an edge of finite level p keeps them together only up to p.139theorem FiniteLevel.together_of_least (V leftEnd rightEnd T g : Set, k n : Nat)140  requires ends : leftEnd(g) ∈ V ∧ rightEnd(g) ∈ V141  requires least : ∀ q ∈ ℕ,142    FiniteLevel(V, leftEnd, rightEnd, T, g, k, q) → n ≤ q143  shows ∃ Y ∈ partitionSequence(V, leftEnd, rightEnd, T, k, n),144    leftEnd(g) ∈ Y ∧ rightEnd(g) ∈ Y145proof146  by_contra apart147  have start := partitionSequence.together_zero148    at V, leftEnd, rightEnd, T, g, k with ends149  obtain ⟨q, natural, less, levelG⟩ :=150    FiniteLevel.of_parted with start, apart151  have below := least with q, natural, levelG152  have qNat := nat.omega.backward with natural153  arith154155theorem FiniteLevel.le_of_together (V E leftEnd rightEnd T g : Set, k n p : Nat)156  requires graph : Graph(V, E, leftEnd, rightEnd)157  requires decomposition : Decomposition(E, T, k)158  requires level : FiniteLevel(V, leftEnd, rightEnd, T, g, k, p)159  requires together :160    ∃ Y ∈ partitionSequence(V, leftEnd, rightEnd, T, k, n),161      leftEnd(g) ∈ Y ∧ rightEnd(g) ∈ Y162  shows n ≤ p163proof164  by_contra above165  have less := Less.of_not_LessEqual with above166  obtain ⟨d, dNat, sum⟩ := less167  rw under ← sum at together168  exact level.right with (partitionSequence.earlier with169    graph, decomposition, together)170171-- Once the sequence has stopped moving it stays, so a stage below a moving172-- stage is moving.173theorem partitionSequence.active (V E leftEnd rightEnd T : Set, k n d : Nat)174  requires graph : Graph(V, E, leftEnd, rightEnd)175  requires nonempty : V ≠ ∅176  requires decomposition : Decomposition(E, T, k)177  requires active : disconnectedColour(leftEnd, rightEnd, T,178    partitionSequence(V, leftEnd, rightEnd, T, k, n + d), k) ≠ ∅179  shows disconnectedColour(leftEnd, rightEnd, T,180    partitionSequence(V, leftEnd, rightEnd, T, k, n), k) ≠ ∅181proof182  intro none183  apply active184  have partition :185      Partition(V, partitionSequence(V, leftEnd, rightEnd, T, k, n)) :=186    partitionSequence.partition with graph, nonempty, decomposition187  have fixed := partitionStep.fixed with partition, none188  rw ← partitionSequence.succ at fixed189  rw (partitionSequence.fixed_from with fixed)190  exact none191192-- Vertices joined by F from inside a set closed under F are joined by the193-- edges of F inside that set.194theorem Joined.inside (leftEnd rightEnd F X u v : Set)195  requires closed : ClosedUnder(leftEnd, rightEnd, F, X)196  requires start : u ∈ X197  requires joined : Joined(leftEnd, rightEnd, F, u, v)198  shows Joined(leftEnd, rightEnd, inside(leftEnd, rightEnd, F, X), u, v)199proof200  intros A inA closedA201  have closedBoth : ClosedUnder(leftEnd, rightEnd, F, A ∩ X)202    intros e inF203    have balanced := closed with e, inF204    by_cases leftX : leftEnd(e) ∈ X205    . have rightX := balanced.forward with leftX206      have insideEdge : e ∈ inside(leftEnd, rightEnd, F, X) :=207        ⟨inF, leftX, rightX⟩208      have balancedA := closedA with e, insideEdge209      rw [intersection.membership, intersection.membership]210      simp [leftX, rightX, balancedA]211    . have rightX : ¬rightEnd(e) ∈ X212        intro inX213        exact leftX with (balanced.backward with inX)214      rw [intersection.membership, intersection.membership]215      simp [leftX, rightX]216  have startBoth : u ∈ A ∩ X :=217    intersection.membership.backward with ⟨inA, start⟩218  have reached := joined with A ∩ X, startBoth, closedBoth219  exact (intersection.membership.forward with reached).left220221-- Ends of an edge in a class X of P that the edges of F inside X join222-- share a class of the refinement of P along F: the component of F within223-- X holding them.224theorem refineBy.together (leftEnd rightEnd F P X e : Set)225  requires class : X ∈ P226  requires ends : leftEnd(e) ∈ X ∧ rightEnd(e) ∈ X227  requires joined : Joined(leftEnd, rightEnd, inside(leftEnd, rightEnd, F, X),228    leftEnd(e), rightEnd(e))229  shows ∃ Y ∈ refineBy(leftEnd, rightEnd, F, P),230    leftEnd(e) ∈ Y ∧ rightEnd(e) ∈ Y231proof232  witness componentBy(X, leftEnd, rightEnd, inside(leftEnd, rightEnd, F, X),233    leftEnd(e))234  refine ⟨?_, ?_, ?_⟩235  . exact refineBy.membership.backward with236      ⟨X, class, (componentsBy.contains with ends.left)⟩237  . exact componentBy.self with ends.left238  . exact ⟨ends.right, joined⟩239240-- An edge of the colour refined at stage m whose ends share a class there241-- keeps them together at stage m + 1: so at the level of an edge some colour242-- is disconnected, and the edge is not of the refining colour.243theorem FiniteLevel.refining_colour (V E leftEnd rightEnd T e : Set, k m : Nat)244  requires graph : Graph(V, E, leftEnd, rightEnd)245  requires nonempty : V ≠ ∅246  requires decomposition : Decomposition(E, T, k)247  requires level : FiniteLevel(V, leftEnd, rightEnd, T, e, k, m)248  shows disconnectedColour(leftEnd, rightEnd, T,249      partitionSequence(V, leftEnd, rightEnd, T, k, m), k) ≠ ∅ ∧250    ¬e ∈ T(leastNatural(disconnectedColour(leftEnd, rightEnd, T,251      partitionSequence(V, leftEnd, rightEnd, T, k, m), k)))252proof253  obtain ⟨together, parted⟩ := level254  obtain ⟨X, class, leftIn, rightIn⟩ := together255  have partition :256      Partition(V, partitionSequence(V, leftEnd, rightEnd, T, k, m)) :=257    partitionSequence.partition with graph, nonempty, decomposition258  have some : disconnectedColour(leftEnd, rightEnd, T,259      partitionSequence(V, leftEnd, rightEnd, T, k, m), k) ≠ ∅260    intro none261    have fixed := partitionStep.fixed with partition, none262    apply parted263    witness X264    rw [partitionSequence.succ, fixed]265    exact ⟨class, leftIn, rightIn⟩266  refine ⟨some, ?_⟩267  intro inColour268  obtain ⟨colour, _⟩ := disconnectedColour.least with some269  have ends := Decomposition.ends with graph, decomposition, colour270  have insideEdge : e ∈ inside(leftEnd, rightEnd,271      T(leastNatural(disconnectedColour(leftEnd, rightEnd, T,272        partitionSequence(V, leftEnd, rightEnd, T, k, m), k))), X) :=273    ⟨inColour, leftIn, rightIn⟩274  have joined := Joined.of_edge at leftEnd, rightEnd, _, _ with insideEdge275  apply parted276  rw under partitionSequence.succ277  rw under partitionStep.refined with partition, ends, some278  exact refineBy.together with class, ⟨leftIn, rightIn⟩, joined279280-- The colour c refined at the level of an edge e of the last colour is a281-- colour below k not holding e, so e closes an even set in the tree T(c).282theorem FiniteLevel.colour_below (V E leftEnd rightEnd T e : Set, c k m : Nat)283  requires graph : Graph(V, E, leftEnd, rightEnd)284  requires nonempty : V ≠ ∅285  requires decomposition : Decomposition(E, T, succ(k))286  requires level : FiniteLevel(V, leftEnd, rightEnd, T, e, succ(k), m)287  requires first : e ∈ T(k)288  requires colour : c = leastNatural(disconnectedColour(leftEnd, rightEnd, T,289    partitionSequence(V, leftEnd, rightEnd, T, succ(k), m), succ(k)))290  shows c ∈ k ∧ ¬e ∈ T(c) ∧ disconnectedColour(leftEnd, rightEnd, T,291    partitionSequence(V, leftEnd, rightEnd, T, succ(k), m), succ(k)) ≠ ∅292proof293  obtain ⟨some, outside⟩ := FiniteLevel.refining_colour with294    graph, nonempty, decomposition, level295  obtain ⟨colourIn, _⟩ := disconnectedColour.least with some296  rw ← colour at outside, colourIn297  have notK : c ≠ k298    intro same299    rw same at outside300    exact outside with first301  have below := Less.of_membership at c, succ(k) with colourIn302  have less := Less.of_successor_upper_ne with below, notK303  exact ⟨(membership.of_Less at c, k with *, less), outside, some⟩304