Grace/Cumulus/GraphTheory/DoubleCover/CompatibilitySystem.g17

Open in Workbench Download source

Imports

Labels

Declarations

Source

1-- The compatibility condition as a parity system: the unknowns are the2-- coordinates of the vertex vectors and one switch per edge, the rows the3-- coordinates of the edges, and a solution gives a compatible assignment.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.DoubleCover.CompatibilitySystem10import Labels1112-- The parity system of the compatibility condition: unknowns are the13-- coordinates (v, i) of the vertex vectors and one switch (e, 3) per edge,14-- tagged so that it never coincides with a vertex coordinate; rows are the15-- coordinates (e, i) of the edges.16def compatibilityMatrix (V E leftEnd rightEnd F : Set) : Set :=17  { p ∈ (E × 3) × ((V × 3) ∪ (E × {3})) | ∃ e ∈ E, ∃ i ∈ 3,18    p = ((e, i), (leftEnd(e), i)) ∨ p = ((e, i), (rightEnd(e), i)) ∨19    (i ∈ flowValue(F, e) ∧ p = ((e, i), (e, 3))) }2021def compatibilitySide (E d : Set) : Set :=22  { p ∈ E × 3 | ∃ e ∈ E, ∃ i ∈ 3, i ∈ d(e) ∧ p = (e, i) }2324-- A coordinate of 3 is not the tag 3.25theorem membership.three.ne (i : Set)26  requires coordinate : i ∈ 327  shows i ≠ 328proof29  have cases := membership.three.forward with coordinate30  rcases cases with rfl | rfl | rfl31  . simp32  . simp33  . simp3435-- The row (e, i) of the matrix meets the two vertex columns of the ends of36-- e and, when i lies in the value of e, the switch column of e.37theorem compatibilityMatrix.row (V E leftEnd rightEnd F e i c : Set)38  requires graph : Graph(V, E, leftEnd, rightEnd)39  requires edge : e ∈ E40  requires coordinate : i ∈ 341  shows ((e, i), c) ∈ compatibilityMatrix(V, E, leftEnd, rightEnd, F) ↔42    (c = (leftEnd(e), i) ∨ c = (rightEnd(e), i) ∨43      (i ∈ flowValue(F, e) ∧ c = (e, 3)))44proof45  have ends := Graph.ends with graph46  obtain ⟨vertexL, vertexR⟩ := ends with e, edge47  constructor48  . intro hp49    obtain ⟨_, x, hx, j, hj, shape⟩ := hp50    rcases shape with h | h | h51    . have parts := orderedPair.injective with h52      have inner := orderedPair.injective with parts.left53      left54      cc55    . have parts := orderedPair.injective with h56      have inner := orderedPair.injective with parts.left57      right58      left59      cc60    . have parts := orderedPair.injective with h.right61      have inner := orderedPair.injective with parts.left62      have value := h.left63      right64      right65      constructor66      . cc67      . cc68  . intro hc69    have row : (e, i) ∈ E × 3 := product.pair with edge, coordinate70    have column : c ∈ (V × 3) ∪ (E × {3})71      rcases hc with h | h | h72      . rw h73        simp [product.pair_membership, vertexL, coordinate]74      . rw h75        simp [product.pair_membership, vertexR, coordinate]76      . rw h.right77        simp [product.pair_membership, edge]78    have shape : ((e, i), c) = ((e, i), (leftEnd(e), i)) ∨79        ((e, i), c) = ((e, i), (rightEnd(e), i)) ∨80        (i ∈ flowValue(F, e) ∧ ((e, i), c) = ((e, i), (e, 3)))81      rcases hc with h | h | h82      . left83        cc84      . right85        left86        cc87      . right88        right89        constructor90        . exact h.left91        . cc92    apply compatibilityMatrix.membership.backward93    exact ⟨(product.pair with row, column), e, edge, i, coordinate, shape⟩9495-- The entries of the row (e, i): the column of either end of e, and the96-- switch column of e exactly when i lies in the value of e.97theorem compatibilityMatrix.end (V E leftEnd rightEnd F e i v : Set)98  requires graph : Graph(V, E, leftEnd, rightEnd)99  requires edge : e ∈ E100  requires coordinate : i ∈ 3101  requires incident : leftEnd(e) = v ∨ rightEnd(e) = v102  shows ((e, i), (v, i)) ∈ compatibilityMatrix(V, E, leftEnd, rightEnd, F)103proof104  rw compatibilityMatrix.row with graph, edge, coordinate105  rcases incident with h | h106  . left107    cc108  . right109    left110    cc111112theorem compatibilityMatrix.switch (V E leftEnd rightEnd F e i : Set)113  requires graph : Graph(V, E, leftEnd, rightEnd)114  requires edge : e ∈ E115  requires coordinate : i ∈ 3116  shows ((e, i), (e, 3)) ∈ compatibilityMatrix(V, E, leftEnd, rightEnd, F) ↔117    i ∈ flowValue(F, e)118proof119  have tag := membership.three.ne with coordinate120  have notL : (e, 3) ≠ (leftEnd(e), i)121    intro same122    apply tag123    symm124    exact (orderedPair.injective with same).right125  have notR : (e, 3) ≠ (rightEnd(e), i)126    intro same127    apply tag128    symm129    exact (orderedPair.injective with same).right130  rw compatibilityMatrix.row with graph, edge, coordinate131  simp [notL, notR]132133theorem compatibilitySide.pair (E d e i : Set)134  requires edge : e ∈ E135  requires coordinate : i ∈ 3136  shows (e, i) ∈ compatibilitySide(E, d) ↔ i ∈ d(e)137proof138  constructor139  . intro hp140    obtain ⟨_, x, hx, j, hj, value, shape⟩ := hp141    have parts := orderedPair.injective with shape142    cc143  . intro value144    apply compatibilitySide.membership.backward145    exact ⟨(product.pair with edge, coordinate), e, edge, i, coordinate,146      value, rfl⟩147148-- The vertex vectors read off a solution t: v ↦ {i ∈ 3 | (v, i) ∈ t}; the149-- switch of e is value(e) when (e, 3) ∈ t and ∅ otherwise.150def coordinates (t v : Set) : Set := { i ∈ 3 | (v, i) ∈ t }151152def vertexVectors (V t : Set) : Set :=153  { p ∈ V × 𝒫(3) | ∃ v ∈ V, p = (v, coordinates(t, v)) }154155def switch (F t e : Set) : Set := { i ∈ flowValue(F, e) | (e, 3) ∈ t }156157theorem coordinates.subset (t v : Set)158  shows coordinates(t, v) ⊆ 3159proof160  intros i hi161  exact hi.left162163theorem vertexVectors.function (V t : Set)164  shows vertexVectors(V, t) : V → 𝒫(3)165proof166  constructor167  . intros p member168    exact member.left169  . constructor170    . intros x y xy z xz171      obtain ⟨_, a, _, shapeY⟩ := xy172      obtain ⟨_, b, _, shapeZ⟩ := xz173      obtain ⟨sameA, valueY⟩ := orderedPair.injective with shapeY174      obtain ⟨sameB, valueZ⟩ := orderedPair.injective with shapeZ175      cc176    . intros v hv177      have inside : coordinates(t, v) ∈ 𝒫(3) :=178        powerset.membership_iff.backward with coordinates.subset179      refine ⟨coordinates(t, v), inside, _⟩180      exact vertexVectors.membership.backward181        with ⟨(product.pair with hv, inside), v, hv, rfl⟩182183theorem vertexVectors.value (V t v : Set)184  requires member : v ∈ V185  shows vertexVectors(V, t)(v) = coordinates(t, v)186proof187  have inside : coordinates(t, v) ∈ 𝒫(3) :=188    powerset.membership_iff.backward with coordinates.subset189  have related : relates(vertexVectors(V, t), v, coordinates(t, v)) :=190    vertexVectors.membership.backward191      with ⟨(product.pair with member, inside), v, member, rfl⟩192  exact FunctionBetween.apply_value193    with vertexVectors.function, member, related194195theorem switch.span (F t e : Set)196  shows switch(F, t, e) ∈ span(flowValue(F, e))197proof198  rw span.membership199  by_cases on : (e, 3) ∈ t200  . right201    ext i202    simp [switch.membership, on]203  . left204    ext i205    simp [switch.membership, on]206207-- A solution of the compatibility system gives compatible vertex vectors:208-- the row (e, i) says that t differs at (leftEnd(e), i) and (rightEnd(e), i)209-- exactly when i ∈ d(e), corrected by the switch when i ∈ value(e).210theorem Compatible.of_solution (V E leftEnd rightEnd F d t : Set)211  requires graph : Graph(V, E, leftEnd, rightEnd)212  requires cubic : Cubic(V, E, leftEnd, rightEnd)213  requires side : FunctionBetween(d, E, 𝒫(3))214  requires solution : Solves(compatibilityMatrix(V, E, leftEnd, rightEnd, F),215    E × 3, (V × 3) ∪ (E × {3}), compatibilitySide(E, d), t)216  shows ∃ u, Compatible(V, E, leftEnd, rightEnd, F, u, d)217proof218  have ends := Graph.ends with graph219  witness vertexVectors(V, t)220  refine ⟨vertexVectors.function, ?_⟩221  intros e he222  obtain ⟨vertexL, vertexR⟩ := ends with e, he223  have loopless := cubic.right with e, he224  have inside : d(e) ⊆ 3 := powerset.membership_iff.forward225    with (FunctionBetween.apply_closed with side, he)226  witness switch(F, t, e)227  refine ⟨switch.span, ?_⟩228  rw [vertexVectors.value with vertexL, vertexVectors.value with vertexR]229  ext i230  rw [symmetricDifference.membership, symmetricDifference.membership]231  by_cases hi : i ∈ 3232  . -- The row (e, i) of the system, read on the three columns it can meet.233    have row : (e, i) ∈ E × 3 := product.pair with he, hi234    have parity := solution.right with (e, i), row235    rw compatibilitySide.pair with he, hi at parity236    have tag := membership.three.ne with hi237    have apartLR : (leftEnd(e), i) ≠ (rightEnd(e), i)238      intro same239      exact loopless with (orderedPair.injective with same).left240    have apartRS : (rightEnd(e), i) ≠ (e, 3)241      intro same242      exact tag with (orderedPair.injective with same).right243    have apartLS : (leftEnd(e), i) ≠ (e, 3)244      intro same245      exact tag with (orderedPair.injective with same).right246    have apart : (leftEnd(e), i) ≠ (rightEnd(e), i) ∧247        (rightEnd(e), i) ≠ (e, 3) ∧ (leftEnd(e), i) ≠ (e, 3) :=248      ⟨apartLR, apartRS, apartLS⟩249    have columns : fiber(compatibilityMatrix(V, E, leftEnd, rightEnd, F),250        (V × 3) ∪ (E × {3}), (e, i)) ∩ t ⊆251        ({(leftEnd(e), i)} ∪ {(rightEnd(e), i)}) ∪ {(e, 3)}252      intros c hc253      have entry := hc.left.right254      rw compatibilityMatrix.row with graph, he, hi at entry255      simp256    rw EvenSet.of_three with apart, columns at parity257    have columnL : (leftEnd(e), i) ∈ (V × 3) ∪ (E × {3})258      by simp [product.pair_membership, vertexL, hi]259    have columnR : (rightEnd(e), i) ∈ (V × 3) ∪ (E × {3})260      by simp [product.pair_membership, vertexR, hi]261    have columnS : (e, 3) ∈ (V × 3) ∪ (E × {3})262      by simp [product.pair_membership, he]263    have atL : leftEnd(e) = leftEnd(e) ∨ rightEnd(e) = leftEnd(e) by simp264    have atR : leftEnd(e) = rightEnd(e) ∨ rightEnd(e) = rightEnd(e) by simp265    have entryL : ((e, i), (leftEnd(e), i)) ∈266        compatibilityMatrix(V, E, leftEnd, rightEnd, F) :=267      compatibilityMatrix.end with graph, he, hi, atL268    have entryR : ((e, i), (rightEnd(e), i)) ∈269        compatibilityMatrix(V, E, leftEnd, rightEnd, F) :=270      compatibilityMatrix.end with graph, he, hi, atR271    have entryS : ((e, i), (e, 3)) ∈272        compatibilityMatrix(V, E, leftEnd, rightEnd, F) ↔273        i ∈ flowValue(F, e) :=274      compatibilityMatrix.switch with graph, he, hi275    simp [fiber.membership, columnL, columnR, columnS, entryL, entryR,276      entryS] at parity277    simp [coordinates.membership, switch.membership, hi]278  . -- Outside 3 none of the four sets holds i.279    have notD : ¬i ∈ d(e)280      intro h281      exact hi with (inside with i, h)282    simp [coordinates.membership, switch.membership, flowValue, hi, notD]283