Grace/Cumulus/GraphTheory/DoubleCover/CubicLabeling.g17

Open in Workbench Download source

Imports

Obstruction · Set.Choice

Declarations

Source

1-- A cubic loopless graph with an even cover has an even double cover indexed2-- by the eight vectors: the compatibility system is unobstructed, so it has3-- a solution, whose vertex vectors are compatible and give the labels.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.CubicLabeling10import Obstruction11import Set.Choice1213-- The base points of e at v, and a chosen sum of base points at the two14-- ends of each edge, as a function on E.15def basePoints (V E leftEnd rightEnd F v e : Set) : Set :=16  { c ∈ 𝒫(3) | BasePoint(V, E, leftEnd, rightEnd, F, v, e, c) }1718def baseSum (V E leftEnd rightEnd F e : Set) : Set :=19  choose(basePoints(V, E, leftEnd, rightEnd, F, leftEnd(e), e)) △20  choose(basePoints(V, E, leftEnd, rightEnd, F, rightEnd(e), e))2122def baseFunction (V E leftEnd rightEnd F : Set) : Set :=23  { p ∈ E × 𝒫(3) | ∃ e ∈ E, p = (e, baseSum(V, E, leftEnd, rightEnd, F, e)) }2425-- The value of another edge at v is a base point of e there.26theorem basePoints.nonempty (V E leftEnd rightEnd F v e : Set)27  requires cubic : Cubic(V, E, leftEnd, rightEnd)28  requires vertex : v ∈ V29  requires edge : e ∈ E30  requires incident : leftEnd(e) = v ∨ rightEnd(e) = v31  shows Nonempty(basePoints(V, E, leftEnd, rightEnd, F, v, e))32proof33  obtain ⟨f, hf, g, hg, distinct, atF, _⟩ :=34    Cubic.others with cubic, vertex, edge, incident35  have inside : flowValue(F, f) ∈ 𝒫(3) :=36    powerset.membership_iff.backward with flowValue.subset37  have fe : f ≠ e by cc38  have point : BasePoint(V, E, leftEnd, rightEnd, F, v, e, flowValue(F, f)) :=39    ⟨f, hf, fe, atF, rfl⟩40  witness flowValue(F, f)41  exact ⟨inside, point⟩4243theorem baseSum.subset (V E leftEnd rightEnd F e : Set)44  requires graph : Graph(V, E, leftEnd, rightEnd)45  requires cubic : Cubic(V, E, leftEnd, rightEnd)46  requires edge : e ∈ E47  shows baseSum(V, E, leftEnd, rightEnd, F, e) ⊆ 348proof49  have ends := Graph.ends with graph50  obtain ⟨vertexL, vertexR⟩ := ends with e, edge51  have atL : leftEnd(e) = leftEnd(e) ∨ rightEnd(e) = leftEnd(e) by simp52  have atR : leftEnd(e) = rightEnd(e) ∨ rightEnd(e) = rightEnd(e) by simp53  have chosenL := choose.member54    with (basePoints.nonempty at _, _, _, _, F, _, _55      with cubic, vertexL, edge, atL)56  have chosenR := choose.member57    with (basePoints.nonempty at _, _, _, _, F, _, _58      with cubic, vertexR, edge, atR)59  have insideL := powerset.membership_iff.forward with chosenL.left60  have insideR := powerset.membership_iff.forward with chosenR.left61  unfold baseSum62  exact symmetricDifference.subset with insideL, insideR6364theorem baseFunction.function (V E leftEnd rightEnd F : Set)65  requires graph : Graph(V, E, leftEnd, rightEnd)66  requires cubic : Cubic(V, E, leftEnd, rightEnd)67  shows baseFunction(V, E, leftEnd, rightEnd, F) : E → 𝒫(3)68proof69  constructor70  . intros p member71    exact member.left72  . constructor73    . intros x y xy z xz74      obtain ⟨_, a, _, shapeY⟩ := xy75      obtain ⟨_, b, _, shapeZ⟩ := xz76      obtain ⟨sameA, valueY⟩ := orderedPair.injective with shapeY77      obtain ⟨sameB, valueZ⟩ := orderedPair.injective with shapeZ78      cc79    . intros e he80      have inside : baseSum(V, E, leftEnd, rightEnd, F, e) ∈ 𝒫(3) :=81        powerset.membership_iff.backward82          with (baseSum.subset with graph, cubic, he)83      refine ⟨baseSum(V, E, leftEnd, rightEnd, F, e), inside, _⟩84      exact baseFunction.membership.backward85        with ⟨(product.pair with he, inside), e, he, rfl⟩8687theorem baseFunction.value (V E leftEnd rightEnd F e : Set)88  requires graph : Graph(V, E, leftEnd, rightEnd)89  requires cubic : Cubic(V, E, leftEnd, rightEnd)90  requires member : e ∈ E91  shows baseFunction(V, E, leftEnd, rightEnd, F)(e) =92    baseSum(V, E, leftEnd, rightEnd, F, e)93proof94  have inside : baseSum(V, E, leftEnd, rightEnd, F, e) ∈ 𝒫(3) :=95    powerset.membership_iff.backward96      with (baseSum.subset with graph, cubic, member)97  have related : relates(baseFunction(V, E, leftEnd, rightEnd, F), e,98      baseSum(V, E, leftEnd, rightEnd, F, e)) :=99    baseFunction.membership.backward100      with ⟨(product.pair with member, inside), e, member, rfl⟩101  have function := baseFunction.function at _, _, _, _, F with graph, cubic102  exact FunctionBetween.apply_value with function, member, related103104-- The chosen sums of base points form a base assignment.105theorem baseFunction.base (V E leftEnd rightEnd F : Set)106  requires graph : Graph(V, E, leftEnd, rightEnd)107  requires cubic : Cubic(V, E, leftEnd, rightEnd)108  shows FunctionBetween(baseFunction(V, E, leftEnd, rightEnd, F), E, 𝒫(3)) ∧109    (∀ e ∈ E, ∃ a, ∃ b,110      BasePoint(V, E, leftEnd, rightEnd, F, leftEnd(e), e, a) ∧111      BasePoint(V, E, leftEnd, rightEnd, F, rightEnd(e), e, b) ∧112      baseFunction(V, E, leftEnd, rightEnd, F)(e) = a △ b)113proof114  have ends := Graph.ends with graph115  constructor116  . exact baseFunction.function at _, _, _, _, F with graph, cubic117  . intros e he118    obtain ⟨vertexL, vertexR⟩ := ends with e, he119    have atL : leftEnd(e) = leftEnd(e) ∨ rightEnd(e) = leftEnd(e) by simp120    have atR : leftEnd(e) = rightEnd(e) ∨ rightEnd(e) = rightEnd(e) by simp121    have chosenL := choose.member122      with (basePoints.nonempty at _, _, _, _, F, _, _123        with cubic, vertexL, he, atL)124    have chosenR := choose.member125      with (basePoints.nonempty at _, _, _, _, F, _, _126        with cubic, vertexR, he, atR)127    have value := baseFunction.value at _, _, _, _, F, _ with graph, cubic, he128    unfold baseSum at value129    witness choose(basePoints(V, E, leftEnd, rightEnd, F, leftEnd(e), e))130    witness choose(basePoints(V, E, leftEnd, rightEnd, F, rightEnd(e), e))131    exact ⟨chosenL.right, chosenR.right, value⟩132133-- A cubic loopless graph with an even cover has an even double cover indexed134-- by the eight vectors: the compatibility system is unobstructed, so it has135-- a solution, whose vertex vectors are compatible and give the labels.136theorem Cubic.even_double_cover (V E leftEnd rightEnd F : Set)137  requires graph : Graph(V, E, leftEnd, rightEnd)138  requires finiteVertices : Finite(V)139  requires finiteEdges : Finite(E)140  requires cubic : Cubic(V, E, leftEnd, rightEnd)141  requires cover : EvenCover(V, E, leftEnd, rightEnd, F)142  shows ∃ H, EvenDoubleCover(V, E, leftEnd, rightEnd, H, 𝒫(3))143proof144  have base := baseFunction.base at _, _, _, _, F with graph, cubic145  have unobstructed := compatibility.unobstructed146    with graph, finiteVertices, finiteEdges, cubic, cover, base147  have finiteThree := Finite.natural at 3148  have finiteRows : Finite(E × 3) :=149    Finite.product with finiteEdges, finiteThree150  have finiteColumns : Finite((V × 3) ∪ (E × {3})) :=151    Finite.union with (Finite.product with finiteVertices, finiteThree),152      (Finite.product with finiteEdges, Finite.singleton)153  have matrix : compatibilityMatrix(V, E, leftEnd, rightEnd, F) ⊆154      (E × 3) × ((V × 3) ∪ (E × {3}))155    intros p hp156    exact hp.left157  have side : compatibilitySide(E, baseFunction(V, E, leftEnd, rightEnd, F)) ⊆158      E × 3159    intros p hp160    exact hp.left161  have alternative := paritySystem.alternative162    with finiteRows, finiteColumns, matrix, side163  obtain ⟨t, solution⟩ := alternative.backward with unobstructed164  obtain ⟨u, compatible⟩ :=165    Compatible.of_solution with graph, cubic, base.left, solution166  obtain ⟨P, function, two, balanced⟩ := Compatible.labels167    with graph, finiteEdges, cubic, cover, base, compatible168  have finiteLabels : Finite(𝒫(3)) := Finite.powerset with finiteThree169  have labels : FunctionBetween(P, E, 𝒫(𝒫(3))) ∧170      (∀ e ∈ E, cardinality(P(e)) = 2) := ⟨function, two⟩171  witness labelFamily(E, P, 𝒫(3))172  exact labels.double_cover173    with graph, finiteEdges, finiteLabels, labels, balanced174