Grace/Cumulus/GraphTheory/DoubleCover/Obstruction.g17

Open in Workbench Download source

Imports

CompatibilitySystem

Declarations

• EvenSet.three_bits theorem derivation
• subset_three.empty_iff theorem derivation
• subset_three.eq_iff theorem derivation
• vertex.parity theorem derivation
• rowSet def
• rowSet.subset theorem derivation
• rowSet.finite theorem derivation
• Obstructs.switch theorem derivation
• Obstructs.vertex theorem derivation
• covered def
• covered.subset theorem derivation
• covered.empty theorem derivation
• covered.insert theorem derivation
• covered.disjoint theorem derivation
• covered.parity theorem derivation
• EvenSet.of_parts theorem derivation
• byFirst def
• atVertex def
• byFirst.pair theorem derivation
• byFirst.of_pair theorem derivation
• atVertex.pair theorem derivation
• byFirst.unique theorem derivation
• byFirst.cover theorem derivation
• incidentEnds.vertex_unique theorem derivation
• atVertex.unique theorem derivation
• atVertex.cover theorem derivation
• atVertex.fiber theorem derivation
• EvenSet.of_two theorem derivation
• EvenSet.intersection_symmetricDifference theorem derivation
• nonzeroEnds def
• OddVertex predicate
• oddEnds def
• nonzeroEnds.subset theorem derivation
• oddEnds.subset theorem derivation
• OddVertex.of_three theorem derivation
• Obstructs.triple_parity theorem derivation
• Obstructs.end_parity theorem derivation
• oddEnds.fiber theorem derivation
• nonzeroEnds.fiber theorem derivation
• nonzeroEnds.even theorem derivation
• Obstructs.edge_parity theorem derivation
• compatibility.unobstructed theorem derivation

Source

1-- The dual obstruction computation: a left-kernel vector of the2-- compatibility system gives at each edge a vector orthogonal to its value,3-- the odd ends regroup over the vertices into an even set, and so no4-- left-kernel vector sees an odd right-hand side.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.Obstruction11import CompatibilitySystem1213-- Parity of a subset of 3 through its three membership bits.14theorem EvenSet.three_bits (X Y : Set)15  requires inside : X ⊆ 316  shows EvenSet(X ∩ Y) ↔17    (((0 ∈ X ∧ 0 ∈ Y) ↔ (1 ∈ X ∧ 1 ∈ Y)) ↔ ¬(2 ∈ X ∧ 2 ∈ Y))18proof19  have apart : 0 ≠ 1 ∧ 1 ≠ 2 ∧ 0 ≠ 2 by simp20  have cover : X ∩ Y ⊆ ({0} ∪ {1}) ∪ {2}21    intros z hz22    have hz3 := inside with z, hz.left23    rw membership.three at hz324    simp25  rw EvenSet.of_three with apart, cover26  simp [intersection.membership]2728theorem subset_three.empty_iff (X : Set)29  requires inside : X ⊆ 330  shows X = ∅ ↔ (¬0 ∈ X ∧ ¬1 ∈ X ∧ ¬2 ∈ X)31proof32  constructor33  . intro empty34    rw empty35    simp36  . intro bits37    ext z38    constructor39    . intro hz40      have hz3 := inside with z, hz41      rw membership.three at hz342      exfalso43      rcases hz3 with rfl | rfl | rfl44      . exact bits.left with hz45      . exact bits.right.left with hz46      . exact bits.right.right with hz47    . intro hz48      simp at hz4950theorem subset_three.eq_iff (X Y : Set)51  requires insideX : X ⊆ 352  requires insideY : Y ⊆ 353  shows X = Y ↔ ((0 ∈ X ↔ 0 ∈ Y) ∧ (1 ∈ X ↔ 1 ∈ Y) ∧ (2 ∈ X ↔ 2 ∈ Y))54proof55  constructor56  . intro same57    rw same58    tauto59  . intro bits60    ext z61    by_cases hz : z ∈ 362    . rw membership.three at hz63      rcases hz with rfl | rfl | rfl64      . exact bits.left65      . exact bits.right.left66      . exact bits.right.right67    . have notX : ¬z ∈ X68        intro h69        exact hz with (insideX with z, h)70      have notY : ¬z ∈ Y71        intro h72        exact hz with (insideY with z, h)73      tauto7475-- The vertex computation of the paper, in the two-element field with three76-- coordinates: at a vertex the three vectors h(e), h(f), h(g) = h(e) △ h(f)77-- are each orthogonal to the matching value, and the values are nonzero and78-- distinct with value(g) = value(e) △ value(f). Then h(e) · value(f) is odd79-- exactly when an odd number of the three h are nonzero.80theorem vertex.parity (he hf hg ve vf vg : Set)81  requires insideE : he ⊆ 382  requires insideF : hf ⊆ 383  requires valueE : ve ⊆ 384  requires valueF : vf ⊆ 385  requires sumH : hg = he △ hf86  requires sumV : vg = ve △ vf87  requires nonzeroE : ve ≠ ∅88  requires nonzeroF : vf ≠ ∅89  requires distinct : ve ≠ vf90  requires orthogonalE : EvenSet(he ∩ ve)91  requires orthogonalF : EvenSet(hf ∩ vf)92  requires orthogonalG : EvenSet(hg ∩ vg)93  shows EvenSet(he ∩ vf) ↔ ((he ≠ ∅ ↔ hf ≠ ∅) ↔ hg = ∅)94proof95  have insideG : hg ⊆ 396    rw sumH97    exact symmetricDifference.subset with insideE, insideF98  have bitsG : ∀ i, (i ∈ hg ↔ ¬(i ∈ he ↔ i ∈ hf))99    intro i100    rw sumH101    exact symmetricDifference.membership102  have bitsV : ∀ i, (i ∈ vg ↔ ¬(i ∈ ve ↔ i ∈ vf))103    intro i104    rw sumV105    exact symmetricDifference.membership106  have g0 := bitsG with 0107  have g1 := bitsG with 1108  have g2 := bitsG with 2109  have v0 := bitsV with 0110  have v1 := bitsV with 1111  have v2 := bitsV with 2112  rw EvenSet.three_bits with insideE at orthogonalE113  rw EvenSet.three_bits with insideF at orthogonalF114  rw EvenSet.three_bits with insideG at orthogonalG115  rw EvenSet.three_bits with insideE116  rw subset_three.empty_iff with valueE at nonzeroE117  rw subset_three.empty_iff with valueF at nonzeroF118  rw subset_three.eq_iff with valueE, valueF at distinct119  rw [subset_three.empty_iff with insideE, subset_three.empty_iff with insideF,120    subset_three.empty_iff with insideG]121  tauto122123-- The vector h(e) of a left-kernel vector y at the edge e.124def rowSet (y e : Set) : Set := { i ∈ 3 | (e, i) ∈ y }125126theorem rowSet.subset (y e : Set)127  shows rowSet(y, e) ⊆ 3128proof129  intros i hi130  exact hi.left131132theorem rowSet.finite (y e : Set)133  shows Finite(rowSet(y, e))134proof135  exact Finite.subset with Finite.natural, rowSet.subset136137-- The switch column of e: y meets it in {e} × (h(e) ∩ value(e)), so h(e) is138-- orthogonal to value(e).139theorem Obstructs.switch (V E leftEnd rightEnd F d y e : Set)140  requires graph : Graph(V, E, leftEnd, rightEnd)141  requires edge : e ∈ E142  requires obstruction : Obstructs(143    compatibilityMatrix(V, E, leftEnd, rightEnd, F), E × 3,144    (V × 3) ∪ (E × {3}), compatibilitySide(E, d), y)145  shows EvenSet(rowSet(y, e) ∩ flowValue(F, e))146proof147  have column : (e, 3) ∈ (V × 3) ∪ (E × {3})148    by simp [product.pair_membership, edge]149  have even := obstruction.right.left with (e, 3), column150  have finite : Finite(rowSet(y, e) ∩ flowValue(F, e)) :=151    Finite.subset with rowSet.finite, intersection.subset_left152  have block : cofiber(compatibilityMatrix(V, E, leftEnd, rightEnd, F),153      E × 3, (e, 3)) ∩ y = {e} × (rowSet(y, e) ∩ flowValue(F, e))154    ext p155    constructor156    . intro hp157      obtain ⟨⟨row, entry⟩, hy⟩ := hp158      obtain ⟨_, x, hx, j, hj, rfl⟩ := product.membership.forward with row159      rw compatibilityMatrix.row with graph, hx, hj at entry160      have tag := membership.three.ne with hj161      rcases entry with h | h | h162      . exfalso163        have parts := orderedPair.injective with h164        apply tag165        cc166      . exfalso167        have parts := orderedPair.injective with h168        apply tag169        cc170      . have parts := orderedPair.injective with h.right171        have xe : x = e by cc172        rw xe at hy, h173        rw xe174        have inRow : j ∈ rowSet(y, e) ∩ flowValue(F, e) := ⟨⟨hj, hy⟩, h.left⟩175        exact product.pair with singleton.self, inRow176    . intro hp177      obtain ⟨_, x, hx, j, hj, rfl⟩ := product.membership.forward with hp178      have xe := singleton.membership.forward with hx179      rw xe180      obtain ⟨⟨hj3, hy⟩, value⟩ := hj181      have entry : ((e, j), (e, 3)) ∈182          compatibilityMatrix(V, E, leftEnd, rightEnd, F) :=183        compatibilityMatrix.switch.backward with graph, edge, hj3, value184      exact ⟨⟨(product.pair with edge, hj3), entry⟩, hy⟩185  rw block at even186  unfold EvenSet at even187  rw cardinality.singleton_product with finite at even188  exact even189190-- A vertex column (v, i) at the vertex v with edges e, f, g: y meets it in191-- the rows (e, i), (f, i), (g, i) it holds, so h(g) = h(e) △ h(f) at v.192theorem Obstructs.vertex (V E leftEnd rightEnd F d y v e f g i : Set)193  requires graph : Graph(V, E, leftEnd, rightEnd)194  requires cubic : Cubic(V, E, leftEnd, rightEnd)195  requires vertex : v ∈ V196  requires edges : e ∈ E ∧ f ∈ E ∧ g ∈ E197  requires incident : (leftEnd(e) = v ∨ rightEnd(e) = v) ∧198    (leftEnd(f) = v ∨ rightEnd(f) = v) ∧199    (leftEnd(g) = v ∨ rightEnd(g) = v)200  requires distinct : e ≠ f ∧ f ≠ g ∧ e ≠ g201  requires coordinate : i ∈ 3202  requires obstruction : Obstructs(203    compatibilityMatrix(V, E, leftEnd, rightEnd, F), E × 3,204    (V × 3) ∪ (E × {3}), compatibilitySide(E, d), y)205  shows i ∈ rowSet(y, g) ↔ ¬(i ∈ rowSet(y, e) ↔ i ∈ rowSet(y, f))206proof207  have column : (v, i) ∈ (V × 3) ∪ (E × {3})208    by simp [product.pair_membership, vertex, coordinate]209  have even := obstruction.right.left with (v, i), column210  have apartEF : (e, i) ≠ (f, i)211    intro same212    exact distinct.left with (orderedPair.injective with same).left213  have apartFG : (f, i) ≠ (g, i)214    intro same215    exact distinct.right.left with (orderedPair.injective with same).left216  have apartEG : (e, i) ≠ (g, i)217    intro same218    exact distinct.right.right with (orderedPair.injective with same).left219  have apart : (e, i) ≠ (f, i) ∧ (f, i) ≠ (g, i) ∧ (e, i) ≠ (g, i) :=220    ⟨apartEF, apartFG, apartEG⟩221  have tag := membership.three.ne with coordinate222  -- A row meeting the column (v, i) is (x, i) for an edge x at v, hence one223  -- of e, f, g.224  have inside : cofiber(compatibilityMatrix(V, E, leftEnd, rightEnd, F),225      E × 3, (v, i)) ∩ y ⊆ ({(e, i)} ∪ {(f, i)}) ∪ {(g, i)}226    intros p hp227    obtain ⟨⟨row, entry⟩, _⟩ := hp228    obtain ⟨_, x, hx, j, hj, rfl⟩ := product.membership.forward with row229    rw compatibilityMatrix.row with graph, hx, hj at entry230    have located : (leftEnd(x) = v ∨ rightEnd(x) = v) ∧ j = i231      rcases entry with h | h | h232      . have parts := orderedPair.injective with h233        constructor234        . left235          cc236        . cc237      . have parts := orderedPair.injective with h238        constructor239        . right240          cc241        . cc242      . exfalso243        have parts := orderedPair.injective with h.right244        apply tag245        cc246    have cases := Cubic.among247      with cubic, vertex, edges, incident, distinct, hx, located.left248    rw located.right249    simp250  rw EvenSet.of_three with apart, inside at even251  have entryE : ((e, i), (v, i)) ∈252      compatibilityMatrix(V, E, leftEnd, rightEnd, F) :=253    compatibilityMatrix.end with graph, edges.left, coordinate, incident.left254  have entryF : ((f, i), (v, i)) ∈255      compatibilityMatrix(V, E, leftEnd, rightEnd, F) :=256    compatibilityMatrix.end257      with graph, edges.right.left, coordinate, incident.right.left258  have entryG : ((g, i), (v, i)) ∈259      compatibilityMatrix(V, E, leftEnd, rightEnd, F) :=260    compatibilityMatrix.end261      with graph, edges.right.right, coordinate, incident.right.right262  have memberE : (e, i) ∈263      cofiber(compatibilityMatrix(V, E, leftEnd, rightEnd, F),264        E × 3, (v, i)) ∩ y ↔ (e, i) ∈ y265    constructor266    . intro hp267      exact hp.right268    . intro hy269      exact ⟨⟨(product.pair with edges.left, coordinate), entryE⟩, hy⟩270  have memberF : (f, i) ∈271      cofiber(compatibilityMatrix(V, E, leftEnd, rightEnd, F),272        E × 3, (v, i)) ∩ y ↔ (f, i) ∈ y273    constructor274    . intro hp275      exact hp.right276    . intro hy277      exact ⟨⟨(product.pair with edges.right.left, coordinate), entryF⟩, hy⟩278  have memberG : (g, i) ∈279      cofiber(compatibilityMatrix(V, E, leftEnd, rightEnd, F),280        E × 3, (v, i)) ∩ y ↔ (g, i) ∈ y281    constructor282    . intro hp283      exact hp.right284    . intro hy285      exact ⟨⟨(product.pair with edges.right.right, coordinate), entryG⟩, hy⟩286  rw [memberE, memberF, memberG] at even287  unfold rowSet288  tauto289290-- Parity of a set partitioned by a finite index: the members of S covered291-- by the indices of G, through a relation P pairing indices with members.292def covered (P S G : Set) : Set := { x ∈ S | ∃ i ∈ G, (i, x) ∈ P }293294theorem covered.subset (P S G : Set)295  shows covered(P, S, G) ⊆ S296proof297  intros x hx298  exact hx.left299300theorem covered.empty (P S : Set)301  shows covered(P, S, ∅) = ∅302proof303  ext x304  simp [covered.membership]305306theorem covered.insert (P S G a : Set)307  shows covered(P, S, G ∪ {a}) = covered(P, S, G) ∪ fiber(P, S, a)308proof309  ext x310  have split : x ∈ covered(P, S, G) ∪ fiber(P, S, a) ↔311      (x ∈ covered(P, S, G) ∨ x ∈ fiber(P, S, a))312    by simp313  rw split314  constructor315  . intro hx316    obtain ⟨hs, i, hi, related⟩ := hx317    simp at hi318    rcases hi with inG | same319    . left320      exact ⟨hs, i, inG, related⟩321    . right322      rw same at related323      exact ⟨hs, related⟩324  . intro hx325    rcases hx with inG | inA326    . obtain ⟨hs, i, hi, related⟩ := inG327      have hi2 : i ∈ G ∪ {a} by simp [hi]328      exact ⟨hs, i, hi2, related⟩329    . have ha : a ∈ G ∪ {a} by simp330      exact ⟨inA.left, a, ha, inA.right⟩331332-- When every member has one index, the part of a fresh index is disjoint333-- from the members covered so far.334theorem covered.disjoint (I P S G a : Set)335  requires unique : ∀ i ∈ I, ∀ j ∈ I, ∀ x, (i, x) ∈ P → (j, x) ∈ P → i = j336  requires inside : G ⊆ I337  requires member : a ∈ I338  requires fresh : ¬a ∈ G339  shows Disjoint(covered(P, S, G), fiber(P, S, a))340proof341  apply Disjoint.iff.backward342  intros x hx hx2343  obtain ⟨_, i, hi, related⟩ := hx344  have same := unique with i, (inside with i, hi), a, member, x, related,345    hx2.right346  rw same at hi347  exact fresh with hi348349theorem covered.parity (I S T P Q : Set)350  requires finiteIndex : Finite(I)351  requires finiteS : Finite(S)352  requires finiteT : Finite(T)353  requires uniqueP : ∀ i ∈ I, ∀ j ∈ I, ∀ x, (i, x) ∈ P → (j, x) ∈ P → i = j354  requires uniqueQ : ∀ i ∈ I, ∀ j ∈ I, ∀ x, (i, x) ∈ Q → (j, x) ∈ Q → i = j355  requires parts : ∀ i ∈ I, (EvenSet(fiber(P, S, i)) ↔ EvenSet(fiber(Q, T, i)))356  shows EvenSet(covered(P, S, I)) ↔ EvenSet(covered(Q, T, I))357proof358  induction finiteIndex with G a359  | empty =>360    rw [covered.empty, covered.empty]361  | insert using ih =>362    rw [covered.insert, covered.insert]363    have finiteGS : Finite(covered(P, S, G)) :=364      Finite.subset with finiteS, covered.subset365    have finiteGT : Finite(covered(Q, T, G)) :=366      Finite.subset with finiteT, covered.subset367    have finiteAS : Finite(fiber(P, S, a)) := fiber.finite with finiteS368    have finiteAT : Finite(fiber(Q, T, a)) := fiber.finite with finiteT369    have apartS := covered.disjoint at _, _, S, _, _370      with uniqueP, GSubset, aMember, aFresh371    have apartT := covered.disjoint at _, _, T, _, _372      with uniqueQ, GSubset, aMember, aFresh373    rw [(EvenSet.union_disjoint with finiteGS, finiteAS, apartS),374      (EvenSet.union_disjoint with finiteGT, finiteAT, apartT)]375    have part := parts with a, aMember376    tauto377378-- Two finite sets partitioned by the same finite index set, with parts of379-- equal parity index by index, have the same parity.380theorem EvenSet.of_parts (I S T P Q : Set)381  requires finiteIndex : Finite(I)382  requires finiteS : Finite(S)383  requires finiteT : Finite(T)384  requires coverS : ∀ x ∈ S, ∃ i ∈ I, (i, x) ∈ P385  requires coverT : ∀ x ∈ T, ∃ i ∈ I, (i, x) ∈ Q386  requires uniqueP : ∀ i ∈ I, ∀ j ∈ I, ∀ x, (i, x) ∈ P → (j, x) ∈ P → i = j387  requires uniqueQ : ∀ i ∈ I, ∀ j ∈ I, ∀ x, (i, x) ∈ Q → (j, x) ∈ Q → i = j388  requires parts : ∀ i ∈ I, (EvenSet(fiber(P, S, i)) ↔ EvenSet(fiber(Q, T, i)))389  shows EvenSet(S) ↔ EvenSet(T)390proof391  have wholeS : covered(P, S, I) = S392    ext x393    constructor394    . intro hx395      exact hx.left396    . intro hx397      exact ⟨hx, (coverS with x, hx)⟩398  have wholeT : covered(Q, T, I) = T399    ext x400    constructor401    . intro hx402      exact hx.left403    . intro hx404      exact ⟨hx, (coverT with x, hx)⟩405  rw [← wholeS, ← wholeT]406  exact covered.parity407    with finiteIndex, finiteS, finiteT, uniqueP, uniqueQ, parts408409-- The two index relations: a pair of I × X indexed by its first entry, and410-- an end indexed by its vertex.411def byFirst (I X : Set) : Set := { q ∈ I × X | fst(snd(q)) = fst(q) }412413def atVertex (V E leftEnd rightEnd : Set) : Set :=414  { q ∈ V × (E × 2) | snd(q) ∈ incidentEnds(leftEnd, rightEnd, E, fst(q)) }415416theorem byFirst.pair (I X i x : Set)417  shows (i, x) ∈ byFirst(I, X) ↔ (i ∈ I ∧ x ∈ X ∧ fst(x) = i)418proof419  simp [byFirst.membership, product.pair_membership, fst.pair, snd.pair]420421-- A pair (e, j) of E × X is indexed by e.422theorem byFirst.of_pair (E X e j : Set)423  requires edge : e ∈ E424  requires member : (e, j) ∈ E × X425  shows (e, (e, j)) ∈ byFirst(E, E × X)426proof427  rw byFirst.pair428  exact ⟨edge, member, fst.pair⟩429430theorem atVertex.pair (V E leftEnd rightEnd v p : Set)431  shows (v, p) ∈ atVertex(V, E, leftEnd, rightEnd) ↔432    (v ∈ V ∧ p ∈ E × 2 ∧ p ∈ incidentEnds(leftEnd, rightEnd, E, v))433proof434  simp [atVertex.membership, product.pair_membership, fst.pair, snd.pair]435436theorem byFirst.unique (I X : Set)437  shows ∀ i ∈ I, ∀ j ∈ I, ∀ x,438    (i, x) ∈ byFirst(I, X) → (j, x) ∈ byFirst(I, X) → i = j439proof440  intros i hi j hj x hix hjx441  rw byFirst.pair at hix, hjx442  cc443444-- Every pair of E × X is indexed by an edge.445theorem byFirst.cover (E X p : Set)446  requires member : p ∈ E × X447  shows ∃ e ∈ E, (e, p) ∈ byFirst(E, E × X)448proof449  obtain ⟨_, e, he, j, hj, rfl⟩ := product.membership.forward with member450  exact ⟨e, he, (byFirst.of_pair with he, member)⟩451452-- An end lies at one vertex.453theorem incidentEnds.vertex_unique (leftEnd rightEnd E v w p : Set)454  requires first : p ∈ incidentEnds(leftEnd, rightEnd, E, v)455  requires second : p ∈ incidentEnds(leftEnd, rightEnd, E, w)456  shows v = w457proof458  obtain ⟨e, he, j, hj, rfl⟩ := incidentEnds.shape with first459  have sidesV := (incidentEnds.pair.forward with first).right460  have sidesW := (incidentEnds.pair.forward with second).right461  have apart : 0 ≠ 1 by simp462  rcases sidesV with ⟨h0, atL⟩ | ⟨h1, atR⟩463  . rcases sidesW with ⟨_, atL2⟩ | ⟨h1, _⟩464    . cc465    . exfalso466      apply apart467      cc468  . rcases sidesW with ⟨h0, _⟩ | ⟨_, atR2⟩469    . exfalso470      apply apart471      cc472    . cc473474theorem atVertex.unique (V E leftEnd rightEnd : Set)475  shows ∀ v ∈ V, ∀ w ∈ V, ∀ p, (v, p) ∈ atVertex(V, E, leftEnd, rightEnd) →476    (w, p) ∈ atVertex(V, E, leftEnd, rightEnd) → v = w477proof478  intros v hv w hw p hvp hwp479  rw atVertex.pair at hvp, hwp480  exact incidentEnds.vertex_unique with hvp.right.right, hwp.right.right481482-- Every end of E lies at a vertex of V.483theorem atVertex.cover (V E leftEnd rightEnd p : Set)484  requires ends : ∀ e ∈ E, leftEnd(e) ∈ V ∧ rightEnd(e) ∈ V485  requires member : p ∈ E × 2486  shows ∃ v ∈ V, (v, p) ∈ atVertex(V, E, leftEnd, rightEnd)487proof488  obtain ⟨_, e, he, j, hj, rfl⟩ := product.membership.forward with member489  obtain ⟨vertexL, vertexR⟩ := ends with e, he490  have cases := membership.two.forward with hj491  rcases cases with rfl | rfl492  . refine ⟨leftEnd(e), vertexL, ?_⟩493    rw atVertex.pair494    refine ⟨vertexL, member, ?_⟩495    simp [incidentEnds.pair, he]496  . refine ⟨rightEnd(e), vertexR, ?_⟩497    rw atVertex.pair498    refine ⟨vertexR, member, ?_⟩499    simp [incidentEnds.pair, he]500501-- The part of a set of pairs at the index v, through atVertex, is its502-- intersection with the ends at v.503theorem atVertex.fiber (V E leftEnd rightEnd S v : Set)504  requires vertex : v ∈ V505  requires pairs : S ⊆ E × 2506  shows fiber(atVertex(V, E, leftEnd, rightEnd), S, v) =507    S ∩ incidentEnds(leftEnd, rightEnd, E, v)508proof509  ext p510  constructor511  . intro hp512    have related := hp.right513    rw atVertex.pair at related514    exact ⟨hp.left, related.right.right⟩515  . intro hp516    have related : (v, p) ∈ atVertex(V, E, leftEnd, rightEnd)517      rw atVertex.pair518      exact ⟨vertex, (pairs with p, hp.left), hp.right⟩519    exact ⟨hp.left, related⟩520521-- Parity of a subset of a two-element set, and of an intersection with a522-- symmetric difference.523theorem EvenSet.of_two (S a b : Set)524  requires apart : a ≠ b525  requires inside : S ⊆ {a} ∪ {b}526  shows EvenSet(S) ↔ (¬a ∈ S ↔ ¬b ∈ S)527proof528  have whole : S ∩ ({a} ∪ {b}) = S := intersection.eq_left_of_subset with inside529  have freshB : ¬b ∈ {a} by simp530  have stepB := EvenSet.intersection_union_part531    at S, {a}, {b}, b with Finite.singleton, Subset.reflexive, freshB532  have stepA : EvenSet(S ∩ {a}) ↔ ¬a ∈ S533    rw intersection.commutative534    exact EvenSet.singleton_intersection535  rw whole at stepB536  rw [stepB, stepA]537  simp538539theorem EvenSet.intersection_symmetricDifference (X A B : Set)540  requires finiteX : Finite(X)541  requires finiteA : Finite(A)542  requires finiteB : Finite(B)543  shows EvenSet(X ∩ (A △ B)) ↔ (EvenSet(X ∩ A) ↔ EvenSet(X ∩ B))544proof545  have step := dot.symmetricDifference with finiteA, finiteB, finiteX546  unfold dot at step547  unfold EvenSet548  rw [intersection.commutative, (intersection.commutative at X, A),549    (intersection.commutative at X, B)]550  exact step551552-- The ends whose edge has a nonzero vector h, the vertices at which an odd553-- number of them meet, and the ends at those vertices.554def nonzeroEnds (E y : Set) : Set := { p ∈ E × 2 | rowSet(y, fst(p)) ≠ ∅ }555556predicate OddVertex (E leftEnd rightEnd y v : Set) :=557  ¬EvenSet(nonzeroEnds(E, y) ∩ incidentEnds(leftEnd, rightEnd, E, v))558559def oddEnds (V E leftEnd rightEnd y : Set) : Set :=560  { p ∈ E × 2 | ∃ v ∈ V, p ∈ incidentEnds(leftEnd, rightEnd, E, v) ∧561    OddVertex(E, leftEnd, rightEnd, y, v) }562563theorem nonzeroEnds.subset (E y : Set)564  shows nonzeroEnds(E, y) ⊆ E × 2565proof566  intros p hp567  exact hp.left568569theorem oddEnds.subset (V E leftEnd rightEnd y : Set)570  shows oddEnds(V, E, leftEnd, rightEnd, y) ⊆ E × 2571proof572  intros p hp573  exact hp.left574575-- At a cubic vertex with edges e, f, g the parity of the nonzero ends is576-- read off the three vectors.577theorem OddVertex.of_three (V E leftEnd rightEnd y v e f g : Set)578  requires cubic : Cubic(V, E, leftEnd, rightEnd)579  requires vertex : v ∈ V580  requires edges : e ∈ E ∧ f ∈ E ∧ g ∈ E581  requires incident : (leftEnd(e) = v ∨ rightEnd(e) = v) ∧582    (leftEnd(f) = v ∨ rightEnd(f) = v) ∧583    (leftEnd(g) = v ∨ rightEnd(g) = v)584  requires distinct : e ≠ f ∧ f ≠ g ∧ e ≠ g585  shows OddVertex(E, leftEnd, rightEnd, y, v) ↔586    ¬((¬rowSet(y, e) ≠ ∅ ↔ ¬rowSet(y, f) ≠ ∅) ↔ ¬rowSet(y, g) ≠ ∅)587proof588  obtain ⟨i, hi, j, hj, k, hk, apart, shape⟩ :=589    Cubic.ends_of_three with cubic, vertex, edges, incident, distinct590  have endE : (e, i) ∈ incidentEnds(leftEnd, rightEnd, E, v) by rw shape; simp591  have endF : (f, j) ∈ incidentEnds(leftEnd, rightEnd, E, v) by rw shape; simp592  have endG : (g, k) ∈ incidentEnds(leftEnd, rightEnd, E, v) by rw shape; simp593  have pairE : (e, i) ∈ E × 2 := product.pair with edges.left, hi594  have pairF : (f, j) ∈ E × 2 := product.pair with edges.right.left, hj595  have pairG : (g, k) ∈ E × 2 := product.pair with edges.right.right, hk596  have inside : nonzeroEnds(E, y) ∩ incidentEnds(leftEnd, rightEnd, E, v) ⊆597      ({(e, i)} ∪ {(f, j)}) ∪ {(g, k)}598    rw ← shape599    intros p hp600    exact hp.right601  unfold OddVertex602  rw EvenSet.of_three with apart, inside603  simp [nonzeroEnds.membership, intersection.membership, pairE, pairF, pairG,604    endE, endF, endG, fst.pair]605606-- The vertex computation for an obstruction: at v with the distinct edges607-- e, x, z, the vector of e is orthogonal to the value of x exactly when an608-- even number of the three vectors are nonzero.609theorem Obstructs.triple_parity (V E leftEnd rightEnd F d y v e x z : Set)610  requires graph : Graph(V, E, leftEnd, rightEnd)611  requires cubic : Cubic(V, E, leftEnd, rightEnd)612  requires cover : EvenCover(V, E, leftEnd, rightEnd, F)613  requires vertex : v ∈ V614  requires edges : e ∈ E ∧ x ∈ E ∧ z ∈ E615  requires incident : (leftEnd(e) = v ∨ rightEnd(e) = v) ∧616    (leftEnd(x) = v ∨ rightEnd(x) = v) ∧617    (leftEnd(z) = v ∨ rightEnd(z) = v)618  requires distinct : e ≠ x ∧ x ≠ z ∧ e ≠ z619  requires obstruction : Obstructs(620    compatibilityMatrix(V, E, leftEnd, rightEnd, F), E × 3,621    (V × 3) ∪ (E × {3}), compatibilitySide(E, d), y)622  shows EvenSet(rowSet(y, e) ∩ flowValue(F, x)) ↔623    ¬OddVertex(E, leftEnd, rightEnd, y, v)624proof625  -- The three vectors sum to zero at v, and so do the three values.626  have sumH : rowSet(y, z) = rowSet(y, e) △ rowSet(y, x)627    ext i628    rw symmetricDifference.membership629    by_cases hi : i ∈ 3630    . exact Obstructs.vertex631        with graph, cubic, vertex, edges, incident, distinct, hi, obstruction632    . simp [rowSet, hi]633  have triple := flowValue.cubic_vertex634    with graph, cubic, cover, vertex, edges, incident, distinct635  have nonzeroE := flowValue.nonzero with cover, edges.left636  have nonzeroX := flowValue.nonzero with cover, edges.right.left637  have orthogonalE := Obstructs.switch with graph, edges.left, obstruction638  have orthogonalX :=639    Obstructs.switch with graph, edges.right.left, obstruction640  have orthogonalZ :=641    Obstructs.switch with graph, edges.right.right, obstruction642  have parity := vertex.parity643    at rowSet(y, e), rowSet(y, x), rowSet(y, z),644      flowValue(F, e), flowValue(F, x), flowValue(F, z)645    with rowSet.subset, rowSet.subset, flowValue.subset, flowValue.subset,646      sumH, triple.right, nonzeroE, nonzeroX, triple.left,647      orthogonalE, orthogonalX, orthogonalZ648  rw [parity,649    (OddVertex.of_three with cubic, vertex, edges, incident, distinct)]650  tauto651652-- The same for any two distinct edges e, x at v.653theorem Obstructs.end_parity (V E leftEnd rightEnd F d y v e x : Set)654  requires graph : Graph(V, E, leftEnd, rightEnd)655  requires cubic : Cubic(V, E, leftEnd, rightEnd)656  requires cover : EvenCover(V, E, leftEnd, rightEnd, F)657  requires vertex : v ∈ V658  requires edge : e ∈ E659  requires incident : leftEnd(e) = v ∨ rightEnd(e) = v660  requires other : x ∈ E ∧ x ≠ e ∧ (leftEnd(x) = v ∨ rightEnd(x) = v)661  requires obstruction : Obstructs(662    compatibilityMatrix(V, E, leftEnd, rightEnd, F), E × 3,663    (V × 3) ∪ (E × {3}), compatibilitySide(E, d), y)664  shows EvenSet(rowSet(y, e) ∩ flowValue(F, x)) ↔665    ¬OddVertex(E, leftEnd, rightEnd, y, v)666proof667  obtain ⟨f, hf, g, hg, distinct, atF, atG⟩ :=668    Cubic.others with cubic, vertex, edge, incident669  have edges : e ∈ E ∧ f ∈ E ∧ g ∈ E := ⟨edge, hf, hg⟩670  have incident3 : (leftEnd(e) = v ∨ rightEnd(e) = v) ∧671      (leftEnd(f) = v ∨ rightEnd(f) = v) ∧672      (leftEnd(g) = v ∨ rightEnd(g) = v) :=673    ⟨incident, atF, atG⟩674  have cases := Cubic.among with cubic, vertex, edges, incident3, distinct,675    other.left, other.right.right676  rcases cases with same | same | same677  . exfalso678    exact other.right.left with same679  . rw same680    exact Obstructs.triple_parity with graph, cubic, cover, vertex, edges,681      incident3, distinct, obstruction682  . rw same683    have edgesG : e ∈ E ∧ g ∈ E ∧ f ∈ E := ⟨edge, hg, hf⟩684    have incidentG : (leftEnd(e) = v ∨ rightEnd(e) = v) ∧685        (leftEnd(g) = v ∨ rightEnd(g) = v) ∧686        (leftEnd(f) = v ∨ rightEnd(f) = v) :=687      ⟨incident, atG, atF⟩688    have gf : g ≠ f by cc689    have distinctG : e ≠ g ∧ g ≠ f ∧ e ≠ f :=690      ⟨distinct.right.right, gf, distinct.left⟩691    exact Obstructs.triple_parity with graph, cubic, cover, vertex, edgesG,692      incidentG, distinctG, obstruction693694-- The parts of the odd ends and of the nonzero ends at a vertex v: all three695-- ends or none, and the nonzero ends at v.696theorem oddEnds.fiber (V E leftEnd rightEnd y v : Set)697  requires cubic : Cubic(V, E, leftEnd, rightEnd)698  requires vertex : v ∈ V699  shows EvenSet(fiber(atVertex(V, E, leftEnd, rightEnd),700      oddEnds(V, E, leftEnd, rightEnd, y), v)) ↔701    ¬OddVertex(E, leftEnd, rightEnd, y, v)702proof703  have pairs : oddEnds(V, E, leftEnd, rightEnd, y) ⊆ E × 2 := oddEnds.subset704  rw atVertex.fiber with vertex, pairs705  by_cases odd : OddVertex(E, leftEnd, rightEnd, y, v)706  . -- Every end at v is odd, and there are three of them.707    have whole : oddEnds(V, E, leftEnd, rightEnd, y) ∩708        incidentEnds(leftEnd, rightEnd, E, v) =709        incidentEnds(leftEnd, rightEnd, E, v)710      ext p711      constructor712      . intro hp713        exact hp.right714      . intro hp715        have product := incidentEnds.subset_product at leftEnd, rightEnd, E, v716        have pair : p ∈ E × 2 := product with p, hp717        exact ⟨⟨pair, v, vertex, hp, odd⟩, hp⟩718    rw whole719    obtain ⟨e, he, f, hf, g, hg, distinct, atE, atF, atG⟩ :=720      Cubic.ends_at with cubic, vertex721    have edges : e ∈ E ∧ f ∈ E ∧ g ∈ E := ⟨he, hf, hg⟩722    have incident : (leftEnd(e) = v ∨ rightEnd(e) = v) ∧723        (leftEnd(f) = v ∨ rightEnd(f) = v) ∧724        (leftEnd(g) = v ∨ rightEnd(g) = v) :=725      ⟨atE, atF, atG⟩726    obtain ⟨i, hi, j, hj, k, hk, apart, shape⟩ :=727      Cubic.ends_of_three with cubic, vertex, edges, incident, distinct728    have inside : incidentEnds(leftEnd, rightEnd, E, v) ⊆729        ({(e, i)} ∪ {(f, j)}) ∪ {(g, k)}730      rw shape731      exact Subset.reflexive732    rw [(EvenSet.of_three with apart, inside), shape]733    simp [odd]734  . -- No end at v is odd.735    have none : oddEnds(V, E, leftEnd, rightEnd, y) ∩736        incidentEnds(leftEnd, rightEnd, E, v) = ∅737      ext p738      constructor739      . intro hp740        obtain ⟨⟨_, w, hw, atW, oddW⟩, atV⟩ := hp741        have same := incidentEnds.vertex_unique with atV, atW742        rw same at odd743        exfalso744        exact odd with oddW745      . intro hp746        simp at hp747    rw none748    simp [EvenSet.empty, odd]749750theorem nonzeroEnds.fiber (V E leftEnd rightEnd y v : Set)751  requires vertex : v ∈ V752  shows EvenSet(fiber(atVertex(V, E, leftEnd, rightEnd), nonzeroEnds(E, y), v))753    ↔ ¬OddVertex(E, leftEnd, rightEnd, y, v)754proof755  have pairs : nonzeroEnds(E, y) ⊆ E × 2 := nonzeroEnds.subset756  rw atVertex.fiber with vertex, pairs757  unfold OddVertex758  tauto759760-- The nonzero ends are even in number: each edge contributes both its ends761-- or neither.762theorem nonzeroEnds.even (E y : Set)763  requires finiteEdges : Finite(E)764  shows EvenSet(nonzeroEnds(E, y))765proof766  have finiteEnds : Finite(E × 2) :=767    Finite.product with finiteEdges, Finite.natural768  have finite : Finite(nonzeroEnds(E, y)) :=769    Finite.subset with finiteEnds, nonzeroEnds.subset770  have cover : ∀ p ∈ nonzeroEnds(E, y), ∃ e ∈ E, (e, p) ∈ byFirst(E, E × 2)771    intros p hp772    exact byFirst.cover with hp.left773  have coverEmpty : ∀ p ∈ ∅, ∃ e ∈ E, (e, p) ∈ byFirst(E, ∅)774    intros p hp775    simp at hp776  -- The part at e is both ends of e or neither.777  have parts : ∀ e ∈ E,778      (EvenSet(fiber(byFirst(E, E × 2), nonzeroEnds(E, y), e)) ↔779        EvenSet(fiber(byFirst(E, ∅), ∅, e)))780    intros e he781    have empty : fiber(byFirst(E, ∅), ∅, e) = ∅782      ext p783      constructor784      . intro hp785        exact hp.left786      . intro hp787        simp at hp788    rw empty789    simp [EvenSet.empty]790    by_cases nonzero : rowSet(y, e) ≠ ∅791    . have whole : fiber(byFirst(E, E × 2), nonzeroEnds(E, y), e) = {e} × 2792        ext p793        constructor794        . intro hp795          have related := hp.right796          rw byFirst.pair at related797          obtain ⟨_, x, hx, j, hj, rfl⟩ :=798            product.membership.forward with hp.left.left799          rw fst.pair at related800          rw related.right.right801          exact product.pair with singleton.self, hj802        . intro hp803          obtain ⟨_, x, hx, j, hj, rfl⟩ := product.membership.forward with hp804          have xe := singleton.membership.forward with hx805          rw xe806          have pair : (e, j) ∈ E × 2 := product.pair with he, hj807          have member : (e, j) ∈ nonzeroEnds(E, y)808            apply nonzeroEnds.membership.backward809            rw fst.pair810            exact ⟨pair, nonzero⟩811          exact ⟨member, (byFirst.of_pair with he, pair)⟩812      rw whole813      unfold EvenSet814      rw [(cardinality.singleton_product with (Finite.natural at 2)),815        (cardinality.natural at 2)]816      exact Even.two817    . have none : fiber(byFirst(E, E × 2), nonzeroEnds(E, y), e) = ∅818        ext p819        constructor820        . intro hp821          have related := hp.right822          rw byFirst.pair at related823          have value := hp.left.right824          rw related.right.right at value825          exfalso826          exact nonzero with value827        . intro hp828          simp at hp829      rw none830      exact EvenSet.empty831  have step := EvenSet.of_parts832    at E, nonzeroEnds(E, y), ∅, byFirst(E, E × 2), byFirst(E, ∅)833    with finiteEdges, finite, Finite.empty, cover, coverEmpty,834      byFirst.unique, byFirst.unique, parts835  rw step836  exact EvenSet.empty837838-- At an edge e: the part of y ∩ side is {e} × (h(e) ∩ d(e)), whose parity839-- is h(e)·a + h(e)·b for base points a, b at the two ends of e; the part of840-- the odd ends holds the ends of e at odd vertices. Both parities agree.841theorem Obstructs.edge_parity (V E leftEnd rightEnd F d y e : Set)842  requires graph : Graph(V, E, leftEnd, rightEnd)843  requires cubic : Cubic(V, E, leftEnd, rightEnd)844  requires cover : EvenCover(V, E, leftEnd, rightEnd, F)845  requires base : FunctionBetween(d, E, 𝒫(3)) ∧ (∀ e ∈ E, ∃ a, ∃ b,846    BasePoint(V, E, leftEnd, rightEnd, F, leftEnd(e), e, a) ∧847    BasePoint(V, E, leftEnd, rightEnd, F, rightEnd(e), e, b) ∧ d(e) = a △ b)848  requires obstruction : Obstructs(849    compatibilityMatrix(V, E, leftEnd, rightEnd, F), E × 3,850    (V × 3) ∪ (E × {3}), compatibilitySide(E, d), y)851  requires edge : e ∈ E852  shows EvenSet(fiber(byFirst(E, E × 3), y ∩ compatibilitySide(E, d), e)) ↔853    EvenSet(fiber(byFirst(E, E × 2), oddEnds(V, E, leftEnd, rightEnd, y), e))854proof855  have ends := Graph.ends with graph856  obtain ⟨vertexL, vertexR⟩ := ends with e, edge857  have atL : leftEnd(e) = leftEnd(e) ∨ rightEnd(e) = leftEnd(e) by simp858  have atR : leftEnd(e) = rightEnd(e) ∨ rightEnd(e) = rightEnd(e) by simp859  -- The part of y ∩ side at e.860  have left : fiber(byFirst(E, E × 3), y ∩ compatibilitySide(E, d), e) =861      {e} × (rowSet(y, e) ∩ d(e))862    ext p863    constructor864    . intro hp865      obtain ⟨⟨hy, hside⟩, related⟩ := hp866      rw byFirst.pair at related867      obtain ⟨_, x, hx, i, hi, rfl⟩ :=868        product.membership.forward with related.right.left869      rw fst.pair at related870      have xe := related.right.right871      rw xe at hy, hside872      rw xe873      rw compatibilitySide.pair with edge, hi at hside874      have inRow : i ∈ rowSet(y, e) ∩ d(e) := ⟨⟨hi, hy⟩, hside⟩875      exact product.pair with singleton.self, inRow876    . intro hp877      obtain ⟨_, x, hx, i, hi, rfl⟩ := product.membership.forward with hp878      have xe := singleton.membership.forward with hx879      rw xe880      obtain ⟨⟨hi3, hy⟩, value⟩ := hi881      have hside : (e, i) ∈ compatibilitySide(E, d)882        rw compatibilitySide.pair with edge, hi3883        exact value884      have pair : (e, i) ∈ E × 3 := product.pair with edge, hi3885      exact ⟨⟨hy, hside⟩, (byFirst.of_pair with edge, pair)⟩886  have finiteRow : Finite(rowSet(y, e) ∩ d(e)) :=887    Finite.subset with rowSet.finite, intersection.subset_left888  have leftParity : EvenSet({e} × (rowSet(y, e) ∩ d(e))) ↔889      EvenSet(rowSet(y, e) ∩ d(e))890    unfold EvenSet891    rw cardinality.singleton_product with finiteRow892  rw [left, leftParity]893  -- d(e) is the sum of base points a = value(x) at the left end and894  -- b = value(z) at the right end.895  obtain ⟨a, b, baseA, baseB, sumD⟩ := base.right with e, edge896  obtain ⟨x, hx, xe, xv, rfl⟩ := baseA897  obtain ⟨z, hz, ze, zv, rfl⟩ := baseB898  rw sumD899  have finiteH := rowSet.finite at y, e900  have finiteX := flowValue.finite at F, x901  have finiteZ := flowValue.finite at F, z902  rw EvenSet.intersection_symmetricDifference with finiteH, finiteX, finiteZ903  have otherX : x ∈ E ∧ x ≠ e ∧904      (leftEnd(x) = leftEnd(e) ∨ rightEnd(x) = leftEnd(e)) := ⟨hx, xe, xv⟩905  have otherZ : z ∈ E ∧ z ≠ e ∧906      (leftEnd(z) = rightEnd(e) ∨ rightEnd(z) = rightEnd(e)) := ⟨hz, ze, zv⟩907  rw [(Obstructs.end_parity908      with graph, cubic, cover, vertexL, edge, atL, otherX, obstruction),909    (Obstructs.end_parity910      with graph, cubic, cover, vertexR, edge, atR, otherZ, obstruction)]911  -- The part of the odd ends at e: among (e, 0) and (e, 1).912  have apart : (e, 0) ≠ (e, 1)913    intro same914    have parts := orderedPair.injective with same915    have zeroOne : 0 ≠ 1 by simp916    exact zeroOne with parts.right917  have inside : fiber(byFirst(E, E × 2), oddEnds(V, E, leftEnd, rightEnd, y), e)918      ⊆ {(e, 0)} ∪ {(e, 1)}919    intros p hp920    have related := hp.right921    rw byFirst.pair at related922    obtain ⟨_, w, hw, j, hj, rfl⟩ :=923      product.membership.forward with related.right.left924    rw fst.pair at related925    have we := related.right.right926    have cases := membership.two.forward with hj927    rw we928    rcases cases with rfl | rfl929    . simp930    . simp931  rw EvenSet.of_two with apart, inside932  have end0 : (e, 0) ∈ incidentEnds(leftEnd, rightEnd, E, leftEnd(e))933    by simp [incidentEnds.pair, edge]934  have end1 : (e, 1) ∈ incidentEnds(leftEnd, rightEnd, E, rightEnd(e))935    by simp [incidentEnds.pair, edge]936  have zero : 0 ∈ 2 by simp [membership.two]937  have one : 1 ∈ 2 by simp [membership.two]938  have pair0 : (e, 0) ∈ E × 2 := product.pair with edge, zero939  have pair1 : (e, 1) ∈ E × 2 := product.pair with edge, one940  have member0 : (e, 0) ∈941      fiber(byFirst(E, E × 2), oddEnds(V, E, leftEnd, rightEnd, y), e) ↔942      OddVertex(E, leftEnd, rightEnd, y, leftEnd(e))943    constructor944    . intro hp945      obtain ⟨⟨_, w, hw, atW, oddW⟩, _⟩ := hp946      have same := incidentEnds.vertex_unique with atW, end0947      rw same at oddW948      exact oddW949    . intro odd950      exact ⟨⟨pair0, leftEnd(e), vertexL, end0, odd⟩,951        (byFirst.of_pair with edge, pair0)⟩952  have member1 : (e, 1) ∈953      fiber(byFirst(E, E × 2), oddEnds(V, E, leftEnd, rightEnd, y), e) ↔954      OddVertex(E, leftEnd, rightEnd, y, rightEnd(e))955    constructor956    . intro hp957      obtain ⟨⟨_, w, hw, atW, oddW⟩, _⟩ := hp958      have same := incidentEnds.vertex_unique with atW, end1959      rw same at oddW960      exact oddW961    . intro odd962      exact ⟨⟨pair1, rightEnd(e), vertexR, end1, odd⟩,963        (byFirst.of_pair with edge, pair1)⟩964  rw [member0, member1]965  tauto966967-- The dual obstruction computation: a left-kernel vector y gives vectors968-- h(e) with h(g) = h(e) △ h(f) at each vertex and h(e) ⊥ value(e); then969-- h(e) · (base point at v) is odd exactly when v is an odd vertex, so y ∩970-- side has the parity of the odd ends, which regroup over the vertices into971-- the nonzero ends, an even set. So y · side is even and y does not obstruct.972theorem compatibility.unobstructed (V E leftEnd rightEnd F d : Set)973  requires graph : Graph(V, E, leftEnd, rightEnd)974  requires finiteVertices : Finite(V)975  requires finiteEdges : Finite(E)976  requires cubic : Cubic(V, E, leftEnd, rightEnd)977  requires cover : EvenCover(V, E, leftEnd, rightEnd, F)978  requires base : FunctionBetween(d, E, 𝒫(3)) ∧ (∀ e ∈ E, ∃ a, ∃ b,979    BasePoint(V, E, leftEnd, rightEnd, F, leftEnd(e), e, a) ∧980    BasePoint(V, E, leftEnd, rightEnd, F, rightEnd(e), e, b) ∧ d(e) = a △ b)981  shows ¬(∃ y, Obstructs(compatibilityMatrix(V, E, leftEnd, rightEnd, F),982    E × 3, (V × 3) ∪ (E × {3}), compatibilitySide(E, d), y))983proof984  intro obstructed985  obtain ⟨y, obstruction⟩ := obstructed986  have ends := Graph.ends with graph987  have rows := obstruction.left988  have finiteRows : Finite(E × 3) :=989    Finite.product with finiteEdges, Finite.natural990  have finiteEnds : Finite(E × 2) :=991    Finite.product with finiteEdges, Finite.natural992  have finiteSide : Finite(y ∩ compatibilitySide(E, d)) :=993    Finite.subset with (Finite.subset with finiteRows, rows),994      intersection.subset_left995  have finiteOdd : Finite(oddEnds(V, E, leftEnd, rightEnd, y)) :=996    Finite.subset with finiteEnds, oddEnds.subset997  have finiteNonzero : Finite(nonzeroEnds(E, y)) :=998    Finite.subset with finiteEnds, nonzeroEnds.subset999  -- Over the edges: y ∩ side has the parity of the odd ends.1000  have coverSide : ∀ p ∈ y ∩ compatibilitySide(E, d), ∃ e ∈ E,1001      (e, p) ∈ byFirst(E, E × 3)1002    intros p hp1003    exact byFirst.cover with (rows with p, hp.left)1004  have coverOdd : ∀ p ∈ oddEnds(V, E, leftEnd, rightEnd, y), ∃ e ∈ E,1005      (e, p) ∈ byFirst(E, E × 2)1006    intros p hp1007    exact byFirst.cover with hp.left1008  have partsEdges : ∀ e ∈ E,1009      (EvenSet(fiber(byFirst(E, E × 3), y ∩ compatibilitySide(E, d), e)) ↔1010        EvenSet(fiber(byFirst(E, E × 2),1011          oddEnds(V, E, leftEnd, rightEnd, y), e)))1012    intros e he1013    exact Obstructs.edge_parity1014      with graph, cubic, cover, base, obstruction, he1015  have stepEdges := EvenSet.of_parts1016    at E, y ∩ compatibilitySide(E, d), oddEnds(V, E, leftEnd, rightEnd, y),1017      byFirst(E, E × 3), byFirst(E, E × 2)1018    with finiteEdges, finiteSide, finiteOdd, coverSide, coverOdd,1019      byFirst.unique, byFirst.unique, partsEdges1020  -- Over the vertices: the odd ends have the parity of the nonzero ends.1021  have coverOddV : ∀ p ∈ oddEnds(V, E, leftEnd, rightEnd, y), ∃ v ∈ V,1022      (v, p) ∈ atVertex(V, E, leftEnd, rightEnd)1023    intros p hp1024    exact atVertex.cover with ends, hp.left1025  have coverNonzeroV : ∀ p ∈ nonzeroEnds(E, y), ∃ v ∈ V,1026      (v, p) ∈ atVertex(V, E, leftEnd, rightEnd)1027    intros p hp1028    exact atVertex.cover with ends, hp.left1029  have partsVertices : ∀ v ∈ V,1030      (EvenSet(fiber(atVertex(V, E, leftEnd, rightEnd),1031        oddEnds(V, E, leftEnd, rightEnd, y), v)) ↔1032      EvenSet(fiber(atVertex(V, E, leftEnd, rightEnd), nonzeroEnds(E, y), v)))1033    intros v hv1034    rw [(oddEnds.fiber with cubic, hv), (nonzeroEnds.fiber with hv)]1035  have stepVertices := EvenSet.of_parts1036    at V, oddEnds(V, E, leftEnd, rightEnd, y), nonzeroEnds(E, y),1037      atVertex(V, E, leftEnd, rightEnd), atVertex(V, E, leftEnd, rightEnd)1038    with finiteVertices, finiteOdd, finiteNonzero, coverOddV, coverNonzeroV,1039      atVertex.unique, atVertex.unique, partsVertices1040  have even := nonzeroEnds.even at E, y with finiteEdges1041  have evenOdd := stepVertices.backward with even1042  have evenSide := stepEdges.backward with evenOdd1043  exact obstruction.right.right with evenSide1044