Grace/Cumulus/GraphTheory/DoubleCover/CubicVertex.g17

Open in Workbench Download source

Imports

Covers · Flows.EvenCovers · Combinatorics.ParityAlternative

Declarations

Source

1-- The values of an even cover at a vertex of a cubic loopless graph: vectors2-- over the two-element field with three coordinates are the subsets of 3, a3-- vertex meets exactly three edge ends, and the three values there are4-- nonzero, distinct, and sum to zero.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.DoubleCover.CubicVertex11import Covers12import Flows.EvenCovers13import Combinatorics.ParityAlternative1415-- Vectors over the two-element field with three coordinates are the subsets16-- of 3; the sum is the symmetric difference, the span of p is {∅, p}.17def span (p : Set) : Set := {∅, p}1819theorem span.membership (p Z : Set)20  shows Z ∈ span(p) ↔ (Z = ∅ ∨ Z = p)21proof22  unfold span23  simp [pair.membership]2425-- The span {∅, p} is closed under sums.26theorem span.sum (p X Y : Set)27  requires first : X ∈ span(p)28  requires second : Y ∈ span(p)29  shows X △ Y ∈ span(p)30proof31  rw span.membership at first, second32  rcases first with rfl | rfl33  . rcases second with rfl | rfl34    . simp [span.membership, symmetricDifference.self]35    . simp [span.membership, symmetricDifference.left_empty]36  . rcases second with rfl | rfl37    . simp [span.membership, symmetricDifference.empty]38    . simp [span.membership, symmetricDifference.self]3940-- The value of an edge is a vector: a subset of 3, hence finite.41theorem flowValue.subset (F e : Set)42  shows flowValue(F, e) ⊆ 343proof44  intros i hi45  exact hi.left4647theorem flowValue.finite (F e : Set)48  shows Finite(flowValue(F, e))49proof50  exact Finite.subset with Finite.natural, flowValue.subset5152-- A set of cardinality three is finite: the selected value of an infinite53-- set is the union of no candidates, which is empty.54theorem Finite.of_cardinality_three (A : Set)55  requires size : cardinality(A) = 356  shows Finite(A)57proof58  by_contra infinite59  unfold cardinality at size60  have none : cardinality.candidates(A) = ∅61    ext n62    constructor63    . intro hn64      obtain ⟨_, has⟩ := hn65      exfalso66      exact infinite with ⟨n, has⟩67    . intro hn68      simp at hn69  rw none at size70  have twoIn : 2 ∈ 3 by simp [membership.three]71  rw ← size at twoIn72  rw union.membership at twoIn73  obtain ⟨y, hy, _⟩ := twoIn74  simp at hy7576-- The parity of a subset of a three-element set, read off its members.77theorem EvenSet.of_three (S a b c : Set)78  requires apart : a ≠ b ∧ b ≠ c ∧ a ≠ c79  requires inside : S ⊆ ({a} ∪ {b}) ∪ {c}80  shows EvenSet(S) ↔ ((¬a ∈ S ↔ ¬b ∈ S) ↔ ¬c ∈ S)81proof82  have whole : S ∩ (({a} ∪ {b}) ∪ {c}) = S :=83    intersection.eq_left_of_subset with inside84  have finitePair : Finite({a} ∪ {b}) :=85    Finite.union with Finite.singleton, Finite.singleton86  have freshC : ¬c ∈ {a} ∪ {b} by simp87  have freshB : ¬b ∈ {a} by simp88  have stepC := EvenSet.intersection_union_part89    at S, {a} ∪ {b}, {c}, c with finitePair, Subset.reflexive, freshC90  have stepB := EvenSet.intersection_union_part91    at S, {a}, {b}, b with Finite.singleton, Subset.reflexive, freshB92  have stepA : EvenSet(S ∩ {a}) ↔ ¬a ∈ S93    rw intersection.commutative94    exact EvenSet.singleton_intersection95  rw whole at stepC96  rw [stepC, stepB, stepA]97  simp9899-- Three distinct members of a three-element set are all of it: removing100-- them in turn leaves nothing.101theorem cardinality.three_members_eq (I a b c : Set)102  requires finite : Finite(I)103  requires size : cardinality(I) = 3104  requires members : a ∈ I ∧ b ∈ I ∧ c ∈ I105  requires apart : a ≠ b ∧ b ≠ c ∧ a ≠ c106  shows I = ({a} ∪ {b}) ∪ {c}107proof108  have finiteA : Finite(I ∖ {a}) := Finite.difference with finite109  have finiteB : Finite((I ∖ {a}) ∖ {b}) := Finite.difference with finiteA110  have finiteC : Finite(((I ∖ {a}) ∖ {b}) ∖ {c}) :=111    Finite.difference with finiteB112  have inA : b ∈ I ∖ {a} by simp [members.right.left, apart.left]113  have inB : c ∈ (I ∖ {a}) ∖ {b}114    by simp [members.right.right, apart.right.left, apart.right.right]115  have removeA := cardinality.remove_add_one with finite, members.left116  have removeB := cardinality.remove_add_one with finiteA, inA117  have removeC := cardinality.remove_add_one with finiteB, inB118  have zero : cardinality(((I ∖ {a}) ∖ {b}) ∖ {c}) = 0 by arith119  have none := cardinality.eq_empty_of_zero with finiteC, zero120  ext x121  constructor122  . intro hx123    by_contra outside124    have inside : x ∈ ((I ∖ {a}) ∖ {b}) ∖ {c} by simp125    rw none at inside126    simp at inside127  . intro hx128    simp at hx129    rcases hx with rfl | rfl | rfl130    . exact members.left131    . exact members.right.left132    . exact members.right.right133134-- An edge at v has an end there.135theorem incidentEnds.end_of (leftEnd rightEnd E v e : Set)136  requires edge : e ∈ E137  requires incident : leftEnd(e) = v ∨ rightEnd(e) = v138  shows ∃ i ∈ 2, (e, i) ∈ incidentEnds(leftEnd, rightEnd, E, v)139proof140  cases incident with atLeft | atRight141  . refine ⟨0, _, _⟩142    . simp [membership.two]143    . simp [incidentEnds.pair, edge, atLeft]144  . refine ⟨1, _, _⟩145    . simp [membership.two]146    . simp [incidentEnds.pair, edge, atRight]147148-- The ends of three distinct edges at a cubic vertex are all of its ends.149theorem Cubic.ends_of_three (V E leftEnd rightEnd v e f g : Set)150  requires cubic : Cubic(V, E, leftEnd, rightEnd)151  requires vertex : v ∈ V152  requires edges : e ∈ E ∧ f ∈ E ∧ g ∈ E153  requires incident : (leftEnd(e) = v ∨ rightEnd(e) = v) ∧154    (leftEnd(f) = v ∨ rightEnd(f) = v) ∧155    (leftEnd(g) = v ∨ rightEnd(g) = v)156  requires distinct : e ≠ f ∧ f ≠ g ∧ e ≠ g157  shows ∃ i ∈ 2, ∃ j ∈ 2, ∃ k ∈ 2,158    ((e, i) ≠ (f, j) ∧ (f, j) ≠ (g, k) ∧ (e, i) ≠ (g, k)) ∧159    incidentEnds(leftEnd, rightEnd, E, v) = ({(e, i)} ∪ {(f, j)}) ∪ {(g, k)}160proof161  obtain ⟨i, hi, endE⟩ := incidentEnds.end_of with edges.left, incident.left162  obtain ⟨j, hj, endF⟩ :=163    incidentEnds.end_of with edges.right.left, incident.right.left164  obtain ⟨k, hk, endG⟩ :=165    incidentEnds.end_of with edges.right.right, incident.right.right166  have degree := cubic.left with v, vertex167  unfold degreeIn at degree168  have finite := Finite.of_cardinality_three with degree169  have apartEF : (e, i) ≠ (f, j)170    intro same171    exact distinct.left with (orderedPair.injective with same).left172  have apartFG : (f, j) ≠ (g, k)173    intro same174    exact distinct.right.left with (orderedPair.injective with same).left175  have apartEG : (e, i) ≠ (g, k)176    intro same177    exact distinct.right.right with (orderedPair.injective with same).left178  have apart : (e, i) ≠ (f, j) ∧ (f, j) ≠ (g, k) ∧ (e, i) ≠ (g, k) :=179    ⟨apartEF, apartFG, apartEG⟩180  have shape := cardinality.three_members_eq181    with finite, degree, ⟨endE, endF, endG⟩, apart182  exact ⟨i, hi, j, hj, k, hk, apart, shape⟩183184-- At a cubic vertex with the distinct edges e, f, g, every edge there is185-- one of them.186theorem Cubic.among (V E leftEnd rightEnd v e f g x : Set)187  requires cubic : Cubic(V, E, leftEnd, rightEnd)188  requires vertex : v ∈ V189  requires edges : e ∈ E ∧ f ∈ E ∧ g ∈ E190  requires incident : (leftEnd(e) = v ∨ rightEnd(e) = v) ∧191    (leftEnd(f) = v ∨ rightEnd(f) = v) ∧192    (leftEnd(g) = v ∨ rightEnd(g) = v)193  requires distinct : e ≠ f ∧ f ≠ g ∧ e ≠ g194  requires edge : x ∈ E195  requires atV : leftEnd(x) = v ∨ rightEnd(x) = v196  shows x = e ∨ x = f ∨ x = g197proof198  obtain ⟨i, hi, j, hj, k, hk, _, shape⟩ :=199    Cubic.ends_of_three with cubic, vertex, edges, incident, distinct200  obtain ⟨m, hm, endX⟩ := incidentEnds.end_of with edge, atV201  rw shape at endX202  simp at endX203  rcases endX with hxe | hxf | hxg204  . left205    exact (orderedPair.injective with hxe).left206  . right207    left208    exact (orderedPair.injective with hxf).left209  . right210    right211    exact (orderedPair.injective with hxg).left212213-- Two ends of a non-loop edge at the same vertex are the same end.214theorem incidentEnds.same_edge (leftEnd rightEnd E v e i j : Set)215  requires loopless : leftEnd(e) ≠ rightEnd(e)216  requires first : (e, i) ∈ incidentEnds(leftEnd, rightEnd, E, v)217  requires second : (e, j) ∈ incidentEnds(leftEnd, rightEnd, E, v)218  shows i = j219proof220  have sidesI := (incidentEnds.pair.forward with first).right221  have sidesJ := (incidentEnds.pair.forward with second).right222  rcases sidesI with ⟨hi, atLeft⟩ | ⟨hi, atRight⟩223  . rcases sidesJ with ⟨hj, _⟩ | ⟨hj, atRight⟩224    . cc225    . exfalso226      apply loopless227      cc228  . rcases sidesJ with ⟨hj, atLeft⟩ | ⟨hj, _⟩229    . exfalso230      apply loopless231      cc232    . cc233234-- Two further edges at an end v of e: removing the end of e from the three235-- ends at v leaves two, and distinct ends at a loopless vertex belong to236-- distinct edges.237theorem Cubic.others (V E leftEnd rightEnd v e : Set)238  requires cubic : Cubic(V, E, leftEnd, rightEnd)239  requires vertex : v ∈ V240  requires edge : e ∈ E241  requires incident : leftEnd(e) = v ∨ rightEnd(e) = v242  shows ∃ f ∈ E, ∃ g ∈ E, (e ≠ f ∧ f ≠ g ∧ e ≠ g) ∧243    (leftEnd(f) = v ∨ rightEnd(f) = v) ∧ (leftEnd(g) = v ∨ rightEnd(g) = v)244proof245  obtain ⟨i, hi, endE⟩ := incidentEnds.end_of with edge, incident246  have degree := cubic.left with v, vertex247  unfold degreeIn at degree248  have finite := Finite.of_cardinality_three with degree249  have removeE := cardinality.remove_add_one with finite, endE250  have finiteRest :251      Finite(incidentEnds(leftEnd, rightEnd, E, v) ∖ {(e, i)}) :=252    Finite.difference with finite253  have positive :254      0 < cardinality(incidentEnds(leftEnd, rightEnd, E, v) ∖ {(e, i)})255    by arith256  obtain ⟨a, ha⟩ := cardinality.member_of_positive with finiteRest, positive257  have removeA := cardinality.remove_add_one with finiteRest, ha258  have finiteRest2 :259      Finite((incidentEnds(leftEnd, rightEnd, E, v) ∖ {(e, i)}) ∖ {a}) :=260    Finite.difference with finiteRest261  have positive2 : 0 <262      cardinality((incidentEnds(leftEnd, rightEnd, E, v) ∖ {(e, i)}) ∖ {a})263    by arith264  obtain ⟨b, hb⟩ := cardinality.member_of_positive with finiteRest2, positive2265  have partsA := difference.singleton_membership.forward with ha266  have partsB := difference.singleton_membership.forward with hb267  have partsB2 := difference.singleton_membership.forward with partsB.left268  obtain ⟨f, hf, j, hj, rfl⟩ := incidentEnds.shape with partsA.left269  obtain ⟨g, hg, k, hk, rfl⟩ := incidentEnds.shape with partsB2.left270  have atF := (incidentEnds.pair.forward with partsA.left).right271  have atG := (incidentEnds.pair.forward with partsB2.left).right272  have ef : e ≠ f273    intro same274    rw ← same at partsA275    have sides := incidentEnds.same_edge276      with (cubic.right with e, edge), partsA.left, endE277    apply partsA.right278    cc279  have eg : e ≠ g280    intro same281    rw ← same at partsB2282    have sides := incidentEnds.same_edge283      with (cubic.right with e, edge), partsB2.left, endE284    apply partsB2.right285    cc286  have fg : f ≠ g287    intro same288    rw same at partsA, partsB289    have sides := incidentEnds.same_edge290      with (cubic.right with g, hg), partsB2.left, partsA.left291    apply partsB.right292    cc293  have incidentF : leftEnd(f) = v ∨ rightEnd(f) = v by tauto294  have incidentG : leftEnd(g) = v ∨ rightEnd(g) = v by tauto295  have distinct : e ≠ f ∧ f ≠ g ∧ e ≠ g := ⟨ef, fg, eg⟩296  exact ⟨f, hf, g, hg, distinct, incidentF, incidentG⟩297298-- Three distinct edges at a cubic vertex.299theorem Cubic.ends_at (V E leftEnd rightEnd v : Set)300  requires cubic : Cubic(V, E, leftEnd, rightEnd)301  requires vertex : v ∈ V302  shows ∃ e ∈ E, ∃ f ∈ E, ∃ g ∈ E, (e ≠ f ∧ f ≠ g ∧ e ≠ g) ∧303    (leftEnd(e) = v ∨ rightEnd(e) = v) ∧304    (leftEnd(f) = v ∨ rightEnd(f) = v) ∧305    (leftEnd(g) = v ∨ rightEnd(g) = v)306proof307  have degree := cubic.left with v, vertex308  unfold degreeIn at degree309  have finite := Finite.of_cardinality_three with degree310  have positive : 0 < cardinality(incidentEnds(leftEnd, rightEnd, E, v))311    by arith312  obtain ⟨a, ha⟩ := cardinality.member_of_positive with finite, positive313  obtain ⟨e, he, i, hi, rfl⟩ := incidentEnds.shape with ha314  have atE := (incidentEnds.pair.forward with ha).right315  have incidentE : leftEnd(e) = v ∨ rightEnd(e) = v by tauto316  obtain ⟨f, hf, g, hg, distinct, incidentF, incidentG⟩ :=317    Cubic.others with cubic, vertex, he, incidentE318  exact ⟨e, he, f, hf, g, hg, distinct, incidentE, incidentF, incidentG⟩319320-- At a cubic vertex the three values are nonzero, pairwise distinct, and321-- their sum vanishes: the third is the sum of the other two.322theorem flowValue.cubic_vertex (V E leftEnd rightEnd F v e f g : Set)323  requires graph : Graph(V, E, leftEnd, rightEnd)324  requires cubic : Cubic(V, E, leftEnd, rightEnd)325  requires cover : EvenCover(V, E, leftEnd, rightEnd, F)326  requires vertex : v ∈ V327  requires edges : e ∈ E ∧ f ∈ E ∧ g ∈ E328  requires incident : (leftEnd(e) = v ∨ rightEnd(e) = v) ∧329    (leftEnd(f) = v ∨ rightEnd(f) = v) ∧330    (leftEnd(g) = v ∨ rightEnd(g) = v)331  requires distinct : e ≠ f ∧ f ≠ g ∧ e ≠ g332  shows flowValue(F, e) ≠ flowValue(F, f) ∧333    flowValue(F, g) = flowValue(F, e) △ flowValue(F, f)334proof335  obtain ⟨i, hi, j, hj, k, hk, apart, shape⟩ :=336    Cubic.ends_of_three with cubic, vertex, edges, incident, distinct337  have endE : (e, i) ∈ incidentEnds(leftEnd, rightEnd, E, v) by rw shape; simp338  have endF : (f, j) ∈ incidentEnds(leftEnd, rightEnd, E, v) by rw shape; simp339  have endG : (g, k) ∈ incidentEnds(leftEnd, rightEnd, E, v) by rw shape; simp340  -- Conservation at v, coordinate by coordinate: the ends carrying x are341  -- even in number, so g carries x exactly when one of e, f does.342  have coordinate : ∀ x ∈ 3, (x ∈ flowValue(F, g) ↔343      ¬(x ∈ flowValue(F, e) ↔ x ∈ flowValue(F, f)))344    intros x hx345    have even := flowValue.conservation with cover, vertex, hx346    have inside : coordinateEnds(leftEnd, rightEnd, E, F, v, x) ⊆347        ({(e, i)} ∪ {(f, j)}) ∪ {(g, k)}348      rw ← shape349      intros p hp350      exact hp.left351    rw EvenSet.of_three with apart, inside at even352    simp [coordinateEnds.membership, endE, endF, endG, fst.pair] at even353    tauto354  have sum : flowValue(F, g) = flowValue(F, e) △ flowValue(F, f)355    ext x356    rw symmetricDifference.membership357    by_cases hx : x ∈ 3358    . exact coordinate with x, hx359    . simp [flowValue, hx]360  constructor361  . -- Equal values at e and f would make the value of g vanish.362    intro same363    have zero : flowValue(F, g) = ∅364      rw [sum, same]365      exact symmetricDifference.self366    have nonzero := flowValue.nonzero with cover, edges.right.right367    exact nonzero with zero368  . exact sum369370-- Two distinct edges at a cubic vertex have distinct values: with the third371-- edge x there, value(f) is value(e) △ value(x), and value(x) is nonzero.372theorem flowValue.cubic_distinct (V E leftEnd rightEnd F v e f : Set)373  requires graph : Graph(V, E, leftEnd, rightEnd)374  requires cubic : Cubic(V, E, leftEnd, rightEnd)375  requires cover : EvenCover(V, E, leftEnd, rightEnd, F)376  requires vertex : v ∈ V377  requires edges : e ∈ E ∧ f ∈ E378  requires incident : (leftEnd(e) = v ∨ rightEnd(e) = v) ∧379    (leftEnd(f) = v ∨ rightEnd(f) = v)380  requires distinct : e ≠ f381  shows flowValue(F, e) ≠ flowValue(F, f)382proof383  obtain ⟨x, hx, z, hz, apart, atX, atZ⟩ :=384    Cubic.others with cubic, vertex, edges.left, incident.left385  have edges3 : e ∈ E ∧ x ∈ E ∧ z ∈ E := ⟨edges.left, hx, hz⟩386  have incident3 : (leftEnd(e) = v ∨ rightEnd(e) = v) ∧387      (leftEnd(x) = v ∨ rightEnd(x) = v) ∧388      (leftEnd(z) = v ∨ rightEnd(z) = v) :=389    ⟨incident.left, atX, atZ⟩390  have triple := flowValue.cubic_vertex391    with graph, cubic, cover, vertex, edges3, incident3, apart392  have nonzeroX := flowValue.nonzero with cover, hx393  have cases := Cubic.among394    with cubic, vertex, edges3, incident3, apart, edges.right, incident.right395  rcases cases with same | same | same396  . cc397  . rw same398    exact triple.left399  . rw same400    intro equal401    apply nonzeroX402    ext i403    have bit := symmetricDifference.membership404      at i, flowValue(F, e), flowValue(F, x)405    rw [← triple.right, ← equal] at bit406    have none : ¬i ∈ flowValue(F, x) by tauto407    simp [none]408