Grace/Cumulus/GraphTheory/TreePacking/LastColour.g17

Open in Workbench Download source

Imports

Levels

Declarations

Source

1-- The even set of a disconnected last colour: on the stable partition the2-- packing condition leaves the last colour enough crossing edges to close a3-- nonempty even set, which holds an edge of finite level.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.LastColour10import Levels1112-- An edge of a colour below j lies in the union of the first j colours.13theorem coloursBelow.contains (T g : Set, j i : Nat)14  requires index : i ∈ j15  requires member : g ∈ T(i)16  shows g ∈ coloursBelow(T, j)17proof18  induction j19  | zero =>20    intro index21    exfalso22    rw nat.zero at index23    exact set.empty with index24  | succ(m) using ih =>25    intro index26    have cases := membership.successor_forward{n := m} with index27    unfold coloursBelow28    rcases cases with earlier | same29    . have inBelow := ih with earlier30      simp [inBelow]31    . rw same at member32      simp [member]3334-- An edge of the first j colours has a colour below j, and the first j35-- colours lie in E.36theorem coloursBelow.colour (T g : Set, j : Nat)37  requires member : g ∈ coloursBelow(T, j)38  shows ∃ i ∈ j, g ∈ T(i)39proof40  induction j41  | zero =>42    intro member43    unfold coloursBelow at member44    exfalso45    exact set.empty with member46  | succ(m) using ih =>47    intro member48    unfold coloursBelow at member49    simp at member50    rcases member with earlier | last51    . obtain ⟨i, index, inT⟩ := ih with earlier52      have inSucc : i ∈ succ(m) by simp [index]53      exact ⟨i, inSucc, inT⟩54    . have self : m ∈ succ(m) by simp55      exact ⟨m, self, last⟩5657-- Two facts about n − 1 beside sub.one_le_of_le_add_one.58theorem sub.one_of_add_one (a b : Nat)59  requires sum : a + 1 = b60  shows b - 1 = a61proof62  have shape := natural.zero_or_successor at b63  rcases shape with zero | ⟨q, natural, rfl⟩64  . rw zero at sum65    arith66  . rw [sub.one, predecessor.succ]67    arith6869theorem sub.le_one_add_one (a : Nat)70  shows a ≤ (a - 1) + 171proof72  have shape := natural.zero_or_successor at a73  rcases shape with zero | ⟨q, natural, rfl⟩74  . rw [zero, sub.zero_left]75    arith76  . rw [sub.one, predecessor.succ]77    arith7879-- The first j trees, each internally connected on P, cross it in at most80-- j(|P| − 1) edges: exactly |P| − 1 each.81theorem coloursBelow.crossing_upper (V E P leftEnd rightEnd T : Set, k j : Nat)82  requires graph : Graph(V, E, leftEnd, rightEnd)83  requires finiteVertices : Finite(V)84  requires finiteEdges : Finite(E)85  requires partition : Partition(V, P)86  requires classes : ∀ i ∈ k, T(i) ⊆ E87  requires trees : ∀ i ∈ k, SpanningTree(V, leftEnd, rightEnd, T(i))88  requires internal :89    ∀ i ∈ k, InternallyConnected(leftEnd, rightEnd, T(i), P)90  requires below : j ≤ k91  shows coloursBelow(T, j) ⊆ E ∧92    cardinality(crossingClasses(P, leftEnd, rightEnd, coloursBelow(T, j))) ≤93      j * (cardinality(P) - 1)94proof95  induction j96  | zero =>97    intro below98    have finiteClasses := Partition.finite with finiteVertices, partition99    unfold coloursBelow100    refine ⟨empty.subset, ?_⟩101    have none : crossingClasses(P, leftEnd, rightEnd, ∅) = ∅102      ext e103      simp [crossingClasses]104    rw [none, cardinality.empty, mul.left_zero]105    arith106  | succ(m) using ih =>107    intro below108    have finiteClasses := Partition.finite with finiteVertices, partition109    have earlier : m ≤ k by arith110    obtain ⟨subsetE, count⟩ := ih with earlier111    have less : m < k by arith112    have inK := membership.of_Less at m, k with *, less113    have classE := classes with m, inK114    have ends := ends_in.subset with (Graph.ends with graph), classE115    have exact := SpanningTree.crossing_count with finiteVertices,116      partition, ends, (trees with m, inK), (internal with m, inK)117    have finiteBelow : Finite(crossingClasses(P, leftEnd, rightEnd,118        coloursBelow(T, m))) :=119      Finite.subset with finiteEdges,120        (Subset.transitive with crossingClasses.subset, subsetE)121    have finiteClass : Finite(crossingClasses(P, leftEnd, rightEnd, T(m))) :=122      Finite.subset with finiteEdges,123        (Subset.transitive with crossingClasses.subset, classE)124    have sum := cardinality.union_le with finiteBelow, finiteClass125    have bound := sub.one_of_add_one with exact126    have step := mul.succ_left at m, cardinality(P) - 1127    unfold coloursBelow128    refine ⟨(Subset.union2_iff.backward with ⟨subsetE, classE⟩), ?_⟩129    rw bound at count130    rw [crossingClasses.union, step, bound]131    arith132133-- The forests inside a finite edge set form a finite family holding ∅.134theorem forestsIn.finite (V leftEnd rightEnd F : Set)135  requires finite : Finite(F)136  shows Finite(forestsIn(V, leftEnd, rightEnd, F))137proof138  have subset : forestsIn(V, leftEnd, rightEnd, F) ⊆ 𝒫(F)139    intros G inFamily140    exact inFamily.left141  exact Finite.subset with (Finite.powerset with finite), subset142143theorem forestsIn.contains_empty (V leftEnd rightEnd F : Set)144  shows ∅ ∈ forestsIn(V, leftEnd, rightEnd, F)145proof146  have forest : Forest(V, leftEnd, rightEnd, ∅)147    constructor148    . exact Finite.empty149    . intros C bound even150      exact Subset.antisymmetric with bound, empty.subset151  exact ⟨(powerset.membership_iff.backward with empty.subset), forest⟩152153-- A maximal forest inside an edge set R joins whatever R joins: an edge of154-- R leaving a component of the forest could be added to it.155theorem Forest.maximal_joined (V leftEnd rightEnd R G u v : Set)156  requires finiteVertices : Finite(V)157  requires ends : ∀ e ∈ R, leftEnd(e) ∈ V ∧ rightEnd(e) ∈ V158  requires member : G ∈ forestsIn(V, leftEnd, rightEnd, R)159  requires maximal :160    ∀ H ∈ forestsIn(V, leftEnd, rightEnd, R), G ⊆ H → H = G161  requires vertex : u ∈ V162  requires joined : Joined(leftEnd, rightEnd, R, u, v)163  shows Joined(leftEnd, rightEnd, G, u, v)164proof165  obtain ⟨inPowerset, forest⟩ := member166  have subsetR := powerset.membership_iff.forward with inPowerset167  have endsG := ends_in.subset with ends, subsetR168  have closedG := componentBy.closed at V, leftEnd, rightEnd, G, u with endsG169  have selfU := componentBy.self at V, leftEnd, rightEnd, G, u with vertex170  have closedR : ClosedUnder(leftEnd, rightEnd, R,171      componentBy(V, leftEnd, rightEnd, G, u))172    intros e inR173    by_contra unbalanced174    have edgeEnds := ends with e, inR175    have outside : ¬e ∈ G176      intro inG177      exact unbalanced with (closedG with e, inG)178    have apartEnds : ¬Joined(leftEnd, rightEnd, G, leftEnd(e), rightEnd(e))179      intro joinedEnds180      exact unbalanced with (Joined.balanced with181        endsG, edgeEnds.left, edgeEnds.right, joinedEnds, closedG)182    have bigger := Forest.add_edge with183      finiteVertices, endsG, edgeEnds, forest, apartEnds184    have biggerSubset : G ∪ {e} ⊆ R := Subset.union2_iff.backward with185      ⟨subsetR, (singleton.subset_iff.backward with inR)⟩186    have biggerIn : G ∪ {e} ∈ forestsIn(V, leftEnd, rightEnd, R) :=187      ⟨(powerset.membership_iff.backward with biggerSubset), bigger⟩188    have equal := maximal with G ∪ {e}, biggerIn, union2.subset_left189    have inBigger : e ∈ G ∪ {e} by simp190    rw equal at inBigger191    exact outside with inBigger192  exact (joined with componentBy(V, leftEnd, rightEnd, G, u), selfU,193    closedR).right194195theorem Forest.maximal_components (V leftEnd rightEnd R G : Set)196  requires finiteVertices : Finite(V)197  requires ends : ∀ e ∈ R, leftEnd(e) ∈ V ∧ rightEnd(e) ∈ V198  requires member : G ∈ forestsIn(V, leftEnd, rightEnd, R)199  requires maximal :200    ∀ H ∈ forestsIn(V, leftEnd, rightEnd, R), G ⊆ H → H = G201  shows componentsBy(V, leftEnd, rightEnd, G) =202    componentsBy(V, leftEnd, rightEnd, R)203proof204  have subsetR := powerset.membership_iff.forward with member.left205  have same : ∀ u ∈ V, componentBy(V, leftEnd, rightEnd, G, u) =206      componentBy(V, leftEnd, rightEnd, R, u)207    intros u vertex208    ext v209    constructor210    . intro inG211      exact ⟨inG.left, (Joined.monotone with subsetR, inG.right)⟩212    . intro inR213      exact ⟨inR.left, (Forest.maximal_joined with214        finiteVertices, ends, member, maximal, vertex, inR.right)⟩215  ext X216  constructor217  . intro inG218    obtain ⟨u, vertex, rfl⟩ := inG219    rw same with u, vertex220    exact componentsBy.contains with vertex221  . intro inR222    obtain ⟨u, vertex, rfl⟩ := inR223    rw ← same with u, vertex224    exact componentsBy.contains with vertex225226-- On a partition P where every colour is internally connected, the packing227-- condition leaves the last colour at least |P| − 1 crossing edges; with a228-- maximal forest of its edges inside the classes, which has the classes as229-- components, these make |V| − 1 edges that do not connect V, so they hold230-- a nonempty even set, which the forest cannot contain.231theorem Kaiser.crossing_cycle (V E P leftEnd rightEnd T : Set, k : Nat)232  requires graph : Graph(V, E, leftEnd, rightEnd)233  requires finiteVertices : Finite(V)234  requires finiteEdges : Finite(E)235  requires partition : Partition(V, P)236  requires decomposition : Decomposition(E, T, succ(k))237  requires trees : ∀ i ∈ k, SpanningTree(V, leftEnd, rightEnd, T(i))238  requires internal :239    ∀ i ∈ succ(k), InternallyConnected(leftEnd, rightEnd, T(i), P)240  requires condition : PackingCondition(V, E, leftEnd, rightEnd, succ(k))241  requires disconnected : ¬Connects(V, leftEnd, rightEnd, T(k))242  shows ∃ C, C ⊆ T(k) ∧ EvenEdgeSet(V, leftEnd, rightEnd, C) ∧243    (∃ e ∈ C, e ∈ crossingClasses(P, leftEnd, rightEnd, T(k)))244proof245  have kIn : k ∈ succ(k) by simp246  have endsE := Graph.ends with graph247  have classK := Decomposition.class_subset with decomposition, kIn248  have endsK := ends_in.subset with endsE, classK249  have finiteK := Finite.subset with finiteEdges, classK250  have finiteClasses := Partition.finite with finiteVertices, partition251  have crossingSubset := crossingClasses.subset at P, leftEnd, rightEnd, T(k)252  have finiteCrossing : Finite(crossingClasses(P, leftEnd, rightEnd, T(k))) :=253    Finite.subset with finiteK, crossingSubset254  -- The last colour crosses P at least |P| − 1 times.255  have classes : ∀ i ∈ k, T(i) ⊆ E256    intros i index257    have iNat := natural.member at k with i, index258    have inSucc : i ∈ succ(k) by simp [index]259    exact Decomposition.class_subset with decomposition, inSucc260  have internalBelow :261      ∀ i ∈ k, InternallyConnected(leftEnd, rightEnd, T(i), P)262    intros i index263    have inSucc : i ∈ succ(k) by simp [index]264    exact internal with i, inSucc265  obtain ⟨belowE, upper⟩ := coloursBelow.crossing_upper with graph,266    finiteVertices, finiteEdges, partition, classes, trees, internalBelow,267    (LessEqual.reflexive at k)268  have cover : E ⊆ coloursBelow(T, k) ∪ T(k)269    intros g inE270    obtain ⟨i, index, inT⟩ := decomposition.right.left with g, inE271    have iNat := natural.member at succ(k) with i, index272    have cases := membership.successor_forward{n := k} with index273    rcases cases with earlier | same274    . have inBelow := coloursBelow.contains with earlier, inT275      simp [inBelow]276    . rw same at inT277      simp [inT]278  have finiteBelow : Finite(crossingClasses(P, leftEnd, rightEnd,279      coloursBelow(T, k))) :=280    Finite.subset with finiteEdges,281      (Subset.transitive with crossingClasses.subset, belowE)282  have covered := crossingClasses.monotone at P, leftEnd, rightEnd, E,283    coloursBelow(T, k) ∪ T(k) with cover284  rw crossingClasses.union at covered285  have boundE := cardinality.monotone with286    (Finite.union with finiteBelow, finiteCrossing), covered287  have sumLe := cardinality.union_le with finiteBelow, finiteCrossing288  have packed := condition with P, partition289  have step := mul.succ_left at k, cardinality(P) - 1290  rw step at packed291  have lowerK : cardinality(P) - 1 ≤292      cardinality(crossingClasses(P, leftEnd, rightEnd, T(k))) by arith293  have lowerP := sub.le_one_add_one at cardinality(P)294  -- A maximal forest among the edges of T(k) inside the classes.295  have restSubset := difference.subset_left296    at T(k), crossingClasses(P, leftEnd, rightEnd, T(k))297  have restFinite := Finite.subset with finiteK, restSubset298  have restEnds := ends_in.subset with endsK, restSubset299  have finiteFamily := forestsIn.finite at V, leftEnd, rightEnd,300    T(k) ∖ crossingClasses(P, leftEnd, rightEnd, T(k)) with restFinite301  have emptyForest := forestsIn.contains_empty at V, leftEnd, rightEnd,302    T(k) ∖ crossingClasses(P, leftEnd, rightEnd, T(k))303  obtain ⟨G, inFamily, _, maximal⟩ :=304    Finite.maximal_extension with finiteFamily, emptyForest305  obtain ⟨inPowerset, forest⟩ := inFamily306  have finiteG := forest.left307  have subsetRest := powerset.membership_iff.forward with inPowerset308  have endsG := ends_in.subset with restEnds, subsetRest309  have components : componentsBy(V, leftEnd, rightEnd, G) = P310    rw ← (componentsBy.eq_classes with311      partition, endsK, (internal with k, kIn))312    exact Forest.maximal_components with313      finiteVertices, restEnds, inFamily, maximal314  have upperG := Forest.edge_bound with finiteVertices, endsG, forest315  have lowerG := componentsBy.lower_bound with finiteVertices, finiteG, endsG316  rw components at upperG, lowerG317  -- The forest with the crossing edges: |V| − 1 edges or more, inside T(k).318  have apart : Disjoint(G, crossingClasses(P, leftEnd, rightEnd, T(k))) :=319    Disjoint.of_subset_left with Disjoint.difference_left, subsetRest320  have sum := cardinality.union_disjoint with finiteG, finiteCrossing, apart321  have subsetK : G ∪ crossingClasses(P, leftEnd, rightEnd, T(k)) ⊆ T(k) :=322    Subset.union2_iff.backward with323      ⟨(Subset.transitive with subsetRest, restSubset), crossingSubset⟩324  have endsF := ends_in.subset with endsK, subsetK325  have finiteF := Finite.subset with finiteK, subsetK326  have dense : cardinality(V) ≤327      cardinality(G ∪ crossingClasses(P, leftEnd, rightEnd, T(k))) + 1328    rw sum329    arith330  have disconnectedF : ¬Connects(V, leftEnd, rightEnd,331      G ∪ crossingClasses(P, leftEnd, rightEnd, T(k)))332    intro connected333    apply disconnected334    intros u hu v hv335    exact Joined.monotone with subsetK, (connected with u, hu, v, hv)336  obtain ⟨C, subsetC, nonemptyC, even⟩ := EvenEdgeSet.of_dense_disconnected337    with finiteVertices, finiteF, endsF, dense, disconnectedF338  -- The even set is not inside the forest, so it holds a crossing edge.339  have escapes : ∃ e ∈ C, ¬e ∈ G340    by_contra none341    have inG : C ⊆ G342      intros e inC343      by_contra outside344      exact none with ⟨e, inC, outside⟩345    exact nonemptyC with (forest.right with C, inG, even)346  obtain ⟨e, inC, outside⟩ := escapes347  have crossing : e ∈ crossingClasses(P, leftEnd, rightEnd, T(k))348    have inF := subsetC with e, inC349    simp at inF350    rcases inF with inG | inCrossing351    . exfalso352      exact outside with inG353    . exact inCrossing354  exact ⟨C, (Subset.transitive with subsetC, subsetK), even,355    e, inC, crossing⟩356357-- When the last colour is disconnected, the packing condition leaves it at358-- least |P_∞| − 1 edges crossing the stable partition, so it contains an359-- even set, and that even set has an edge of finite level.360theorem Kaiser.cycle_edge (V E leftEnd rightEnd T : Set, k : Nat)361  requires graph : Graph(V, E, leftEnd, rightEnd)362  requires finiteVertices : Finite(V)363  requires finiteEdges : Finite(E)364  requires nonempty : V ≠ ∅365  requires decomposition : Decomposition(E, T, succ(k))366  requires trees : ∀ i ∈ k, SpanningTree(V, leftEnd, rightEnd, T(i))367  requires condition : PackingCondition(V, E, leftEnd, rightEnd, succ(k))368  requires disconnected : ¬Connects(V, leftEnd, rightEnd, T(k))369  shows ∃ C, C ⊆ T(k) ∧ EvenEdgeSet(V, leftEnd, rightEnd, C) ∧370    (∃ e ∈ C, ∃ n ∈ ℕ,371      FiniteLevel(V, leftEnd, rightEnd, T, e, succ(k), n))372proof373  have partition :374      Partition(V, stablePartition(V, leftEnd, rightEnd, T, succ(k)))375    unfold stablePartition376    exact partitionSequence.partition with graph, nonempty, decomposition377  have internal := stablePartition.internal with378    graph, finiteVertices, nonempty, decomposition379  obtain ⟨C, subsetC, even, e, inC, crossing⟩ := Kaiser.crossing_cycle with380    graph, finiteVertices, finiteEdges, partition, decomposition, trees,381    internal, condition, disconnected382  have kIn : k ∈ succ(k) by simp383  have ends := Decomposition.ends with graph, decomposition, kIn384  obtain ⟨n, natural, _, level⟩ := FiniteLevel.of_crossing with385    finiteVertices, partition, (ends with e, (subsetC with e, inC)), crossing386  exact ⟨C, subsetC, even, e, inC, n, natural, level⟩387