Grace/Cumulus/GraphTheory/DoubleCover/Labels.g17

Open in Workbench Download source

Imports

CubicVertex

Declarations

Source

1-- Labels from a compatible assignment: the local base point of an edge end2-- is the value of another edge at that vertex, and vertex vectors whose3-- differences along the edges are compatible with the base points give4-- two-element labels with even local multiplicity, hence an even double5-- cover.6-- Part of Cumulus, the Grace17 mathematics library.7-- Copyright (c) 2026 Grant Passmore.8-- Released under the Apache License 2.0. See LICENSE in the repository root.9-- Authors: Grant Passmore1011module Grace.Cumulus.GraphTheory.DoubleCover.Labels12import CubicVertex1314-- The local base point of an end: the value of one other edge at that vertex,15-- determined up to the span of the edge's own value.16predicate BasePoint (V E leftEnd rightEnd F v e c : Set) :=17  ∃ f ∈ E, f ≠ e ∧ (leftEnd(f) = v ∨ rightEnd(f) = v) ∧18    c = flowValue(F, f)1920-- Vertex vectors t with t(u) △ t(v) ∈ d(e) + span(value(e)) for every edge21-- e = uv, where d(e) is the sum of the two base points of e.22predicate Compatible (V E leftEnd rightEnd F t d : Set) :=23  FunctionBetween(t, V, 𝒫(3)) ∧24  (∀ e ∈ E, ∃ s ∈ span(flowValue(F, e)),25    t(leftEnd(e)) △ t(rightEnd(e)) = d(e) △ s)2627-- Sums in the two-element field cancel.28theorem symmetricDifference.cancel_right (A B : Set)29  shows (A △ B) △ B = A30proof31  ext z32  simp3334theorem symmetricDifference.cancel_left (A B C : Set)35  requires same : A △ B = A △ C36  shows B = C37proof38  ext z39  have bit := symmetricDifference.membership at z, A, B40  rw [same, symmetricDifference.membership] at bit41  tauto4243-- Moving x to y by (a △ b) △ s moves x △ u to y △ w by the corrections44-- a △ u and b △ w and s.45theorem symmetricDifference.shift (x y u w a b s : Set)46  requires move : x △ y = (a △ b) △ s47  shows y △ w = (x △ u) △ (((a △ u) △ (b △ w)) △ s)48proof49  ext z50  have bit := symmetricDifference.membership at z, x, y51  rw move at bit52  simp [symmetricDifference.membership]5354-- A base point of e at v, the value of some other edge x there, differs from55-- the value of a fixed other edge f by an element of the span of value(e):56-- either x = f, or e, x, f are the three edges at v.57theorem BasePoint.span (V E leftEnd rightEnd F v e f c : Set)58  requires graph : Graph(V, E, leftEnd, rightEnd)59  requires cubic : Cubic(V, E, leftEnd, rightEnd)60  requires cover : EvenCover(V, E, leftEnd, rightEnd, F)61  requires vertex : v ∈ V62  requires edge : e ∈ E63  requires incident : leftEnd(e) = v ∨ rightEnd(e) = v64  requires other : f ∈ E ∧ f ≠ e ∧ (leftEnd(f) = v ∨ rightEnd(f) = v)65  requires base : BasePoint(V, E, leftEnd, rightEnd, F, v, e, c)66  shows c △ flowValue(F, f) ∈ span(flowValue(F, e))67proof68  obtain ⟨x, hx, xe, xv, rfl⟩ := base69  rw span.membership70  by_cases same : x = f71  . left72    rw same73    exact symmetricDifference.self74  . right75    have edges : e ∈ E ∧ x ∈ E ∧ f ∈ E := ⟨edge, hx, other.left⟩76    have incident3 : (leftEnd(e) = v ∨ rightEnd(e) = v) ∧77        (leftEnd(x) = v ∨ rightEnd(x) = v) ∧78        (leftEnd(f) = v ∨ rightEnd(f) = v) :=79      ⟨incident, xv, other.right.right⟩80    have ex : e ≠ x by cc81    have ef : e ≠ f by cc82    have distinct : e ≠ x ∧ x ≠ f ∧ e ≠ f := ⟨ex, same, ef⟩83    have triple := flowValue.cubic_vertex84      with graph, cubic, cover, vertex, edges, incident3, distinct85    rw triple.right86    ext z87    simp8889-- The labels of e read at its end v: t(v) △ value(x) for the other edges90-- x at v. The label pair of e is read at its left end.91def labelsAt (E leftEnd rightEnd F t v e : Set) : Set :=92  { q ∈ 𝒫(3) | ∃ x ∈ E, x ≠ e ∧ (leftEnd(x) = v ∨ rightEnd(x) = v) ∧93    q = t(v) △ flowValue(F, x) }9495def labelPairs (E leftEnd rightEnd F t : Set) : Set :=96  { p ∈ E × 𝒫(𝒫(3)) | ∃ e ∈ E,97    p = (e, labelsAt(E, leftEnd, rightEnd, F, t, leftEnd(e), e)) }9899theorem labelsAt.subset (E leftEnd rightEnd F t v e : Set)100  shows labelsAt(E, leftEnd, rightEnd, F, t, v, e) ⊆ 𝒫(3)101proof102  intros q hq103  exact hq.left104105theorem labelPairs.function (E leftEnd rightEnd F t : Set)106  shows labelPairs(E, leftEnd, rightEnd, F, t) : E → 𝒫(𝒫(3))107proof108  constructor109  . intros p member110    exact member.left111  . constructor112    . intros x y xy z xz113      obtain ⟨_, a, _, shapeY⟩ := xy114      obtain ⟨_, b, _, shapeZ⟩ := xz115      obtain ⟨sameA, valueY⟩ := orderedPair.injective with shapeY116      obtain ⟨sameB, valueZ⟩ := orderedPair.injective with shapeZ117      cc118    . intros e he119      have inside :120          labelsAt(E, leftEnd, rightEnd, F, t, leftEnd(e), e) ∈ 𝒫(𝒫(3)) :=121        powerset.membership_iff.backward with labelsAt.subset122      refine ⟨labelsAt(E, leftEnd, rightEnd, F, t, leftEnd(e), e), inside, _⟩123      exact labelPairs.membership.backward124        with ⟨(product.pair with he, inside), e, he, rfl⟩125126theorem labelPairs.value (E leftEnd rightEnd F t e : Set)127  requires member : e ∈ E128  shows labelPairs(E, leftEnd, rightEnd, F, t)(e) =129    labelsAt(E, leftEnd, rightEnd, F, t, leftEnd(e), e)130proof131  have inside :132      labelsAt(E, leftEnd, rightEnd, F, t, leftEnd(e), e) ∈ 𝒫(𝒫(3)) :=133    powerset.membership_iff.backward with labelsAt.subset134  have related : relates(labelPairs(E, leftEnd, rightEnd, F, t), e,135      labelsAt(E, leftEnd, rightEnd, F, t, leftEnd(e), e)) :=136    labelPairs.membership.backward137      with ⟨(product.pair with member, inside), e, member, rfl⟩138  exact FunctionBetween.apply_value139    with labelPairs.function, member, related140141-- With the other edges f, g at v, the labels of e at v are t(v) △ value(f)142-- and t(v) △ value(g).143theorem labelsAt.pair (V E leftEnd rightEnd F t v e f g : Set)144  requires cubic : Cubic(V, E, leftEnd, rightEnd)145  requires vertex : v ∈ V146  requires function : FunctionBetween(t, V, 𝒫(3))147  requires edges : e ∈ E ∧ f ∈ E ∧ g ∈ E148  requires incident : (leftEnd(e) = v ∨ rightEnd(e) = v) ∧149    (leftEnd(f) = v ∨ rightEnd(f) = v) ∧150    (leftEnd(g) = v ∨ rightEnd(g) = v)151  requires distinct : e ≠ f ∧ f ≠ g ∧ e ≠ g152  shows labelsAt(E, leftEnd, rightEnd, F, t, v, e) =153    {t(v) △ flowValue(F, f), t(v) △ flowValue(F, g)}154proof155  have vector : t(v) ⊆ 3 := powerset.membership_iff.forward156    with (FunctionBetween.apply_closed with function, vertex)157  have insideF : t(v) △ flowValue(F, f) ∈ 𝒫(3) :=158    powerset.membership_iff.backward159      with (symmetricDifference.subset with vector, flowValue.subset)160  have insideG : t(v) △ flowValue(F, g) ∈ 𝒫(3) :=161    powerset.membership_iff.backward162      with (symmetricDifference.subset with vector, flowValue.subset)163  have fe : f ≠ e by cc164  have ge : g ≠ e by cc165  ext q166  simp [pair.membership]167  constructor168  . intro hq169    obtain ⟨_, x, hx, xe, xv, rfl⟩ := hq170    have cases :=171      Cubic.among with cubic, vertex, edges, incident, distinct, hx, xv172    rcases cases with hxe | hxf | hxg173    . exfalso174      exact xe with hxe175    . left176      cc177    . right178      cc179  . intro hq180    rcases hq with rfl | rfl181    . exact ⟨insideF, f, edges.right.left, fe, incident.right.left, rfl⟩182    . exact ⟨insideG, g, edges.right.right, ge, incident.right.right, rfl⟩183184-- The labels of e read at either end agree: compatibility moves t across e185-- by the sum of two base points and an element of the span of value(e),186-- and each base point differs from the chosen other value by such an187-- element too.188theorem labelsAt.ends (V E leftEnd rightEnd F t d e : Set)189  requires graph : Graph(V, E, leftEnd, rightEnd)190  requires cubic : Cubic(V, E, leftEnd, rightEnd)191  requires cover : EvenCover(V, E, leftEnd, rightEnd, F)192  requires base : FunctionBetween(d, E, 𝒫(3)) ∧ (∀ e ∈ E, ∃ a, ∃ b,193    BasePoint(V, E, leftEnd, rightEnd, F, leftEnd(e), e, a) ∧194    BasePoint(V, E, leftEnd, rightEnd, F, rightEnd(e), e, b) ∧ d(e) = a △ b)195  requires compatible : Compatible(V, E, leftEnd, rightEnd, F, t, d)196  requires edge : e ∈ E197  shows labelsAt(E, leftEnd, rightEnd, F, t, rightEnd(e), e) =198    labelsAt(E, leftEnd, rightEnd, F, t, leftEnd(e), e)199proof200  have ends := Graph.ends with graph201  obtain ⟨vertexL, vertexR⟩ := ends with e, edge202  have atL : leftEnd(e) = leftEnd(e) ∨ rightEnd(e) = leftEnd(e) by simp203  have atR : leftEnd(e) = rightEnd(e) ∨ rightEnd(e) = rightEnd(e) by simp204  obtain ⟨f, hf, g, hg, distinctL, atF, atG⟩ :=205    Cubic.others with cubic, vertexL, edge, atL206  obtain ⟨f2, hf2, g2, hg2, distinctR, atF2, atG2⟩ :=207    Cubic.others with cubic, vertexR, edge, atR208  have edgesL : e ∈ E ∧ f ∈ E ∧ g ∈ E := ⟨edge, hf, hg⟩209  have incidentL : (leftEnd(e) = leftEnd(e) ∨ rightEnd(e) = leftEnd(e)) ∧210      (leftEnd(f) = leftEnd(e) ∨ rightEnd(f) = leftEnd(e)) ∧211      (leftEnd(g) = leftEnd(e) ∨ rightEnd(g) = leftEnd(e)) :=212    ⟨atL, atF, atG⟩213  have edgesR : e ∈ E ∧ f2 ∈ E ∧ g2 ∈ E := ⟨edge, hf2, hg2⟩214  have incidentR : (leftEnd(e) = rightEnd(e) ∨ rightEnd(e) = rightEnd(e)) ∧215      (leftEnd(f2) = rightEnd(e) ∨ rightEnd(f2) = rightEnd(e)) ∧216      (leftEnd(g2) = rightEnd(e) ∨ rightEnd(g2) = rightEnd(e)) :=217    ⟨atR, atF2, atG2⟩218  rw [(labelsAt.pair219      with cubic, vertexL, compatible.left, edgesL, incidentL, distinctL),220    (labelsAt.pair221      with cubic, vertexR, compatible.left, edgesR, incidentR, distinctR)]222  -- At each end the second label is the first shifted by value(e).223  have tripleL := flowValue.cubic_vertex224    with graph, cubic, cover, vertexL, edgesL, incidentL, distinctL225  have tripleR := flowValue.cubic_vertex226    with graph, cubic, cover, vertexR, edgesR, incidentR, distinctR227  have secondL : t(leftEnd(e)) △ flowValue(F, g) =228      (t(leftEnd(e)) △ flowValue(F, f)) △ flowValue(F, e)229    rw tripleL.right230    ext z231    simp232  have secondR : t(rightEnd(e)) △ flowValue(F, g2) =233      (t(rightEnd(e)) △ flowValue(F, f2)) △ flowValue(F, e)234    rw tripleR.right235    ext z236    simp237  -- The first label at the right end is the first at the left end shifted238  -- by (a △ value(f)) △ (b △ value(f2)) △ s, a sum of three elements of239  -- the span of value(e).240  obtain ⟨s, hs, equation⟩ := compatible.right with e, edge241  obtain ⟨a, b, baseA, baseB, sumD⟩ := base.right with e, edge242  have fe : f ≠ e by cc243  have f2e : f2 ≠ e by cc244  have otherF : f ∈ E ∧ f ≠ e ∧245      (leftEnd(f) = leftEnd(e) ∨ rightEnd(f) = leftEnd(e)) := ⟨hf, fe, atF⟩246  have otherF2 : f2 ∈ E ∧ f2 ≠ e ∧247      (leftEnd(f2) = rightEnd(e) ∨ rightEnd(f2) = rightEnd(e)) :=248    ⟨hf2, f2e, atF2⟩249  have spanA := BasePoint.span250    with graph, cubic, cover, vertexL, edge, atL, otherF, baseA251  have spanB := BasePoint.span252    with graph, cubic, cover, vertexR, edge, atR, otherF2, baseB253  have inSpan := span.sum with (span.sum with spanA, spanB), hs254  have move : t(leftEnd(e)) △ t(rightEnd(e)) = (a △ b) △ s255    rw [equation, sumD]256  have shift := symmetricDifference.shift257    at t(leftEnd(e)), t(rightEnd(e)), flowValue(F, f), flowValue(F, f2),258      a, b, s with move259  rw [secondL, secondR, shift]260  rw span.membership at inSpan261  rcases inSpan with zero | full262  . rw [zero, symmetricDifference.empty]263  . rw [full, symmetricDifference.cancel_right]264    exact pair.commutative265266-- From compatible vertex vectors, the label pair of an edge e = uv is267-- {t(u) △ c, t(u) △ c △ value(e)} for a base point c of u at e; the pair268-- is independent of the end and the base point, and at each vertex every269-- label is carried by an even number of the three ends.270theorem Compatible.labels (V E leftEnd rightEnd F t d : Set)271  requires graph : Graph(V, E, leftEnd, rightEnd)272  requires finiteEdges : Finite(E)273  requires cubic : Cubic(V, E, leftEnd, rightEnd)274  requires cover : EvenCover(V, E, leftEnd, rightEnd, F)275  requires base : FunctionBetween(d, E, 𝒫(3)) ∧ (∀ e ∈ E, ∃ a, ∃ b,276    BasePoint(V, E, leftEnd, rightEnd, F, leftEnd(e), e, a) ∧277    BasePoint(V, E, leftEnd, rightEnd, F, rightEnd(e), e, b) ∧ d(e) = a △ b)278  requires compatible : Compatible(V, E, leftEnd, rightEnd, F, t, d)279  shows ∃ P, FunctionBetween(P, E, 𝒫(𝒫(3))) ∧280    (∀ e ∈ E, cardinality(P(e)) = 2) ∧281    (∀ v ∈ V, ∀ s ∈ 𝒫(3),282      EvenSet(labelledEnds(leftEnd, rightEnd, E, P, v, s)))283proof284  have ends := Graph.ends with graph285  have function := labelPairs.function at E, leftEnd, rightEnd, F, t286  -- The label pair of an edge x, read at either end v of x.287  have atEnd : ∀ v ∈ V, ∀ x ∈ E, (leftEnd(x) = v ∨ rightEnd(x) = v) →288      labelPairs(E, leftEnd, rightEnd, F, t)(x) =289        labelsAt(E, leftEnd, rightEnd, F, t, v, x)290    intros v hv x hx xv291    rw labelPairs.value with hx292    have same := labelsAt.ends with graph, cubic, cover, base, compatible, hx293    cases xv with atLeft | atRight294    . cc295    . cc296  witness labelPairs(E, leftEnd, rightEnd, F, t)297  refine ⟨function, ?_, ?_⟩298  . -- Two labels per edge: the other two edges at its left end have299    -- distinct values.300    intros e he301    obtain ⟨vertexL, _⟩ := ends with e, he302    have atL : leftEnd(e) = leftEnd(e) ∨ rightEnd(e) = leftEnd(e) by simp303    obtain ⟨f, hf, g, hg, distinct, atF, atG⟩ :=304      Cubic.others with cubic, vertexL, he, atL305    have edges : e ∈ E ∧ f ∈ E ∧ g ∈ E := ⟨he, hf, hg⟩306    have incident : (leftEnd(e) = leftEnd(e) ∨ rightEnd(e) = leftEnd(e)) ∧307        (leftEnd(f) = leftEnd(e) ∨ rightEnd(f) = leftEnd(e)) ∧308        (leftEnd(g) = leftEnd(e) ∨ rightEnd(g) = leftEnd(e)) :=309      ⟨atL, atF, atG⟩310    rw [(atEnd with leftEnd(e), vertexL, e, he, atL),311      (labelsAt.pair312        with cubic, vertexL, compatible.left, edges, incident, distinct)]313    have values : flowValue(F, f) ≠ flowValue(F, g) :=314      flowValue.cubic_distinct with graph, cubic, cover, vertexL,315        ⟨hf, hg⟩, ⟨atF, atG⟩, distinct.right.left316    have different :317        t(leftEnd(e)) △ flowValue(F, f) ≠ t(leftEnd(e)) △ flowValue(F, g)318      intro same319      exact values with (symmetricDifference.cancel_left with same)320    exact cardinality.pair with different321  . -- At a vertex with edges e, f, g, the label t(v) △ value(x) is carried322    -- by the two ends other than that of x, and no other label is carried.323    intros v hv s hs324    obtain ⟨e, he, f, hf, g, hg, distinct, atE, atF, atG⟩ :=325      Cubic.ends_at with cubic, hv326    have edges : e ∈ E ∧ f ∈ E ∧ g ∈ E := ⟨he, hf, hg⟩327    have incident : (leftEnd(e) = v ∨ rightEnd(e) = v) ∧328        (leftEnd(f) = v ∨ rightEnd(f) = v) ∧329        (leftEnd(g) = v ∨ rightEnd(g) = v) :=330      ⟨atE, atF, atG⟩331    obtain ⟨i, hi, j, hj, k, hk, apart, shape⟩ :=332      Cubic.ends_of_three with cubic, hv, edges, incident, distinct333    have inside : labelledEnds(leftEnd, rightEnd, E,334        labelPairs(E, leftEnd, rightEnd, F, t), v, s) ⊆335        ({(e, i)} ∪ {(f, j)}) ∪ {(g, k)}336      rw ← shape337      intros p hp338      exact hp.left339    rw EvenSet.of_three with apart, inside340    have endE : (e, i) ∈ incidentEnds(leftEnd, rightEnd, E, v) by rw shape; simp341    have endF : (f, j) ∈ incidentEnds(leftEnd, rightEnd, E, v) by rw shape; simp342    have endG : (g, k) ∈ incidentEnds(leftEnd, rightEnd, E, v) by rw shape; simp343    -- The three label pairs, read at v.344    have fe : f ≠ e by cc345    have ge : g ≠ e by cc346    have gf : g ≠ f by cc347    have edgesF : f ∈ E ∧ e ∈ E ∧ g ∈ E := ⟨hf, he, hg⟩348    have incidentF : (leftEnd(f) = v ∨ rightEnd(f) = v) ∧349        (leftEnd(e) = v ∨ rightEnd(e) = v) ∧350        (leftEnd(g) = v ∨ rightEnd(g) = v) :=351      ⟨atF, atE, atG⟩352    have distinctF : f ≠ e ∧ e ≠ g ∧ f ≠ g :=353      ⟨fe, distinct.right.right, distinct.right.left⟩354    have edgesG : g ∈ E ∧ e ∈ E ∧ f ∈ E := ⟨hg, he, hf⟩355    have incidentG : (leftEnd(g) = v ∨ rightEnd(g) = v) ∧356        (leftEnd(e) = v ∨ rightEnd(e) = v) ∧357        (leftEnd(f) = v ∨ rightEnd(f) = v) :=358      ⟨atG, atE, atF⟩359    have distinctG : g ≠ e ∧ e ≠ f ∧ g ≠ f := ⟨ge, distinct.left, gf⟩360    have pairE : labelPairs(E, leftEnd, rightEnd, F, t)(e) =361        {t(v) △ flowValue(F, f), t(v) △ flowValue(F, g)}362      rw atEnd with v, hv, e, he, atE363      exact labelsAt.pair364        with cubic, hv, compatible.left, edges, incident, distinct365    have pairF : labelPairs(E, leftEnd, rightEnd, F, t)(f) =366        {t(v) △ flowValue(F, e), t(v) △ flowValue(F, g)}367      rw atEnd with v, hv, f, hf, atF368      exact labelsAt.pair369        with cubic, hv, compatible.left, edgesF, incidentF, distinctF370    have pairG : labelPairs(E, leftEnd, rightEnd, F, t)(g) =371        {t(v) △ flowValue(F, e), t(v) △ flowValue(F, f)}372      rw atEnd with v, hv, g, hg, atG373      exact labelsAt.pair374        with cubic, hv, compatible.left, edgesG, incidentG, distinctG375    -- The three labels are distinct, as the three values are.376    have neEF := flowValue.cubic_distinct377      with graph, cubic, cover, hv, ⟨he, hf⟩, ⟨atE, atF⟩, distinct.left378    have neFG := flowValue.cubic_distinct379      with graph, cubic, cover, hv, ⟨hf, hg⟩, ⟨atF, atG⟩, distinct.right.left380    have neEG := flowValue.cubic_distinct381      with graph, cubic, cover, hv, ⟨he, hg⟩, ⟨atE, atG⟩, distinct.right.right382    have apartEF : t(v) △ flowValue(F, e) ≠ t(v) △ flowValue(F, f)383      intro same384      exact neEF with (symmetricDifference.cancel_left with same)385    have apartFG : t(v) △ flowValue(F, f) ≠ t(v) △ flowValue(F, g)386      intro same387      exact neFG with (symmetricDifference.cancel_left with same)388    have apartEG : t(v) △ flowValue(F, e) ≠ t(v) △ flowValue(F, g)389      intro same390      exact neEG with (symmetricDifference.cancel_left with same)391    simp [labelledEnds.membership, endE, endF, endG, fst.pair,392      pairE, pairF, pairG, pair.membership]393