Grace/Cumulus/GraphTheory/DoubleCover/EvenDoubleCover.g17

Open in Workbench Download source

Imports

CubicLabeling · Projection · Flows.EightFlow

Declarations

Source

1-- Every finite bridgeless multigraph has an even double cover: over its2-- active vertices a rotation system expands it to a cubic bridgeless graph,3-- the eight-flow theorem gives the expansion an even cover, its labelling4-- gives an even double cover, and the cover projects back.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.EvenDoubleCover11import CubicLabeling12import Projection13import Flows.EightFlow1415-- The vertices at an end of some edge. An isolated vertex has no end to16-- expand, so the expansion is taken over the active vertices alone, and a17-- cover found there is a cover of the whole graph.18def activeVertices (V E leftEnd rightEnd : Set) : Set :=19  { v ∈ V | ∃ e ∈ E, leftEnd(e) = v ∨ rightEnd(e) = v }2021theorem activeVertices.subset (V E leftEnd rightEnd : Set)22  shows activeVertices(V, E, leftEnd, rightEnd) ⊆ V23proof24  intros v hv25  exact hv.left2627theorem activeVertices.graph (V E leftEnd rightEnd : Set)28  requires graph : Graph(V, E, leftEnd, rightEnd)29  shows Graph(activeVertices(V, E, leftEnd, rightEnd), E, leftEnd, rightEnd)30proof31  have ends := Graph.ends with graph32  constructor33  . have values : ∀ e ∈ E,34        leftEnd(e) ∈ activeVertices(V, E, leftEnd, rightEnd)35      intros e he36      refine ⟨(ends with e, he).left, e, he, _⟩37      left38      rfl39    exact FunctionBetween.codomain_of_values with graph.left, values40  . have values : ∀ e ∈ E,41        rightEnd(e) ∈ activeVertices(V, E, leftEnd, rightEnd)42      intros e he43      refine ⟨(ends with e, he).right, e, he, _⟩44      right45      rfl46    exact FunctionBetween.codomain_of_values with graph.right, values4748-- Bridgelessness is inherited by the active vertices, as every vertex set49-- of theirs is one of V.50theorem activeVertices.bridgeless (V E leftEnd rightEnd : Set)51  requires bridgeless : Bridgeless(V, E, leftEnd, rightEnd)52  shows Bridgeless(activeVertices(V, E, leftEnd, rightEnd), E,53    leftEnd, rightEnd)54proof55  intros X bound56  exact bridgeless with X, (Subset.transitive with bound, activeVertices.subset)5758-- An active vertex of a bridgeless graph has degree at least two: it has an59-- end, and a bridgeless graph has no vertex of degree one.60theorem activeVertices.degrees (V E leftEnd rightEnd : Set)61  requires graph : Graph(V, E, leftEnd, rightEnd)62  requires finiteEdges : Finite(E)63  requires bridgeless : Bridgeless(V, E, leftEnd, rightEnd)64  shows ∀ v ∈ activeVertices(V, E, leftEnd, rightEnd),65    2 ≤ degreeIn(leftEnd, rightEnd, E, v)66proof67  intros v hv68  obtain ⟨vertex, e, he, atEnd⟩ := hv69  have finiteEnds := incidentEnds.finite at leftEnd, rightEnd, E, v70    with finiteEdges71  have notOne :=72    Bridgeless.degrees with graph, finiteEdges, bridgeless, v, vertex73  have notZero : degreeIn(leftEnd, rightEnd, E, v) ≠ 074    unfold degreeIn75    cases atEnd with atLeft | atRight76    . have end : (e, 0) ∈ incidentEnds(leftEnd, rightEnd, E, v)77        simp [incidentEnds.pair, he, atLeft]78      exact cardinality.ne_zero_of_member with finiteEnds, end79    . have end : (e, 1) ∈ incidentEnds(leftEnd, rightEnd, E, v)80        simp [incidentEnds.pair, he, atRight]81      exact cardinality.ne_zero_of_member with finiteEnds, end82  have natural := degreeIn.natural at leftEnd, rightEnd, E, v with finiteEdges83  have zeroLe : 0 ≤ degreeIn(leftEnd, rightEnd, E, v) by arith84  have apart : 0 ≠ degreeIn(leftEnd, rightEnd, E, v) by cc85  have positive : 0 < degreeIn(leftEnd, rightEnd, E, v) :=86    Less.of_LessEqual_ne with zeroLe, apart87  have above : 1 < degreeIn(leftEnd, rightEnd, E, v) :=88    Less.successor_lower_of_ne with positive, notOne89  arith9091-- An edge set even over the active vertices is even over all of them: an92-- isolated vertex has degree zero in every edge set.93theorem EvenEdgeSet.of_active (V E leftEnd rightEnd F : Set)94  requires edges : F ⊆ E95  requires even : EvenEdgeSet(activeVertices(V, E, leftEnd, rightEnd),96    leftEnd, rightEnd, F)97  shows EvenEdgeSet(V, leftEnd, rightEnd, F)98proof99  constructor100  . exact even.left101  . intros v hv102    by_cases active : v ∈ activeVertices(V, E, leftEnd, rightEnd)103    . exact even.right with v, active104    . have none : incidentEnds(leftEnd, rightEnd, F, v) = ∅105        apply Subset.antisymmetric106        . intros p hp107          obtain ⟨e, he, i, hi, rfl⟩ := incidentEnds.shape with hp108          have sides := (incidentEnds.pair.forward with hp).right109          exfalso110          apply active111          refine ⟨hv, e, (edges with e, he), _⟩112          tauto113        . exact empty.subset114      unfold degreeIn115      rw [none, cardinality.empty]116      exact Even.zero117118theorem EvenDoubleCover.of_active (V E leftEnd rightEnd H I : Set)119  requires cover : EvenDoubleCover(activeVertices(V, E, leftEnd, rightEnd),120    E, leftEnd, rightEnd, H, I)121  shows EvenDoubleCover(V, E, leftEnd, rightEnd, H, I)122proof123  obtain ⟨finiteIndex, family, evens, twice⟩ := cover124  refine ⟨finiteIndex, family, _, twice⟩125  intros i hi126  have edges : H(i) ⊆ E :=127    powerset.membership.forward128      with (FunctionBetween.apply_closed with family, hi)129  exact EvenEdgeSet.of_active with edges, (evens with i, hi)130131-- A finite bridgeless graph has an even double cover. Over its active132-- vertices it is bridgeless with every degree at least two, so a rotation133-- system expands it to a finite cubic bridgeless graph; the eight-flow134-- theorem gives the expansion an even cover, its labelling gives an even135-- double cover, and the cover projects back along the spokes.136theorem Bridgeless.even_double_cover (V E leftEnd rightEnd : Set)137  requires graph : Graph(V, E, leftEnd, rightEnd)138  requires finiteVertices : Finite(V)139  requires finiteEdges : Finite(E)140  requires bridgeless : Bridgeless(V, E, leftEnd, rightEnd)141  shows ∃ H, ∃ I, EvenDoubleCover(V, E, leftEnd, rightEnd, H, I)142proof143  have active := activeVertices.graph with graph144  have finiteActive : Finite(activeVertices(V, E, leftEnd, rightEnd)) :=145    Finite.subset with finiteVertices, activeVertices.subset146  have bridgelessActive := activeVertices.bridgeless with bridgeless147  have degrees := activeVertices.degrees with graph, finiteEdges, bridgeless148  obtain ⟨σ, rotation⟩ :=149    RotationSystem.exists with active, finiteActive, finiteEdges150  have expanded := expansion.graph with active, rotation151  have finiteEnds := halfEdges.finite with finiteEdges152  have finiteExpanded := expandedEdges.finite with finiteEdges153  have cubic := expansion.cubic with active, finiteEdges, rotation, degrees154  have expandedBridgeless := expansion.bridgeless155    with active, finiteActive, finiteEdges, rotation, bridgelessActive156  obtain ⟨F, cover⟩ :=157    eightFlow with expanded, finiteEnds, finiteExpanded, expandedBridgeless158  obtain ⟨H, double⟩ := Cubic.even_double_cover159    with expanded, finiteEnds, finiteExpanded, cubic, cover160  have projected :=161    projected.double_cover with active, finiteEdges, rotation, double162  exact ⟨projectedFamily(E, H, 𝒫(3)), 𝒫(3),163    (EvenDoubleCover.of_active with projected)⟩164