Cycles, acyclicity and bridges

This file sits directly on Schoenflies/Graph/Walk.lean and answers one question: which edges of a multigraph lie on a cycle. Its main theorem is the blueprint's cycle criterion — an edge lies on a cycle exactly when deleting it leaves its two ends joined — and a bridge is read off it.

A cycle is presented through one of its edges

G.IsCycleThrough e u v D is an edge e linking u to v, together with a path D from u to v that does not use e. The closed walk is never assembled.

This is not a weakening. Every question the blueprint asks about a cycle is asked at an edge — is this edge on a cycle, does deleting it disconnect its ends, is it a bridge, can it be deleted from a spanning subgraph — so the edge is always available to present the cycle through. And presenting it this way is what makes the definition short: the blueprint's "connected subgraph in which every vertex has degree exactly two" would have to rule out, by hand, every repetition that a closed walk can contain, whereas Graph.IsPath already forbids them. The blueprint's own proof of the criterion runs in exactly this shape ("take a shortest walk from x to y avoiding e; a shortest walk repeats no vertex, so it is a simple path").

Length two is included, and is why edges are names. Two parallel edges — the same pair of ends, two different names — are a cycle: one of them is e, the other is the one-edge path D. The blueprint needs those ("two-vertex cycles do occur below, as boundaries of faces created by overlays and by ears parallel to an existing edge"), and a walk that named vertices could not tell the two apart.

Loops

Mathlib's Graph allows an edge with both ends equal. A loop is taken to be a cycle of length one, which is the usual convention and also what the blueprint's own definition gives (a loop contributes two to the degree of its vertex, so the subgraph consisting of a loop and its vertex is connected with every vertex of degree two). It comes out of the definition here for free: G.IsLink e x x together with the empty path at x, which does not use e, is a cycle through e. So Graph.liesOnCycle_of_isLoopAt needs no proof, no graph is acyclic while carrying a loop, and no bridge is a loop. Nothing in this file hypothesises looplessness.

Deletion

Edge deletion is Mathlib's Graph.deleteEdges, not a new definition; G.deleteEdges {e} is the graph with the single name e removed. What this file adds is the transfer interface — a walk or a path survives a deletion exactly when it never took a deleted edge — which is the whole content of a deletion argument, since which vertices an edge joins is not a question a subgraph can answer differently. Graph.IsWalk.anti from Walk.lean is the engine; Graph.IsPath.anti is proved here, since freshness has to be carried down too.

Blueprint

• Graph.liesOnCycle_iff_deleteEdges_reaches — lem:cycle-criterion, "in a finite graph, an edge lies on a cycle if and only if deleting it does not disconnect its endpoints", both directions, with the finiteness the proof does not use dropped. The two halves are Graph.LiesOnCycle.deleteEdges_reaches and Graph.LiesOnCycle.of_deleteEdges_reaches.
• Graph.IsBridge, Graph.isBridge_iff_not_reaches — the bridges of lem:subdivision-ear-preserve ("a 2-connected graph has no bridge. Indeed, if uv were a bridge, the two components of G - uv …"), stated as the separation of the two ends.
• Graph.IsAcyclic, Graph.Connected.deleteEdges_singleton — the acyclicity underneath lem:three-leaf-tree, and the minimal spanning subgraph of the H5 construction ("take a minimal connected subgraph T_i spanning the three terminals. It is a tree: an edge of a cycle could be deleted"), which is exactly the statement that deleting an edge on a cycle keeps the graph connected.
• Graph.IsPath.chord_liesOnCycle, Graph.IsAcyclic.mem_of_isLink_of_mem_walkVertices — the step of lem:three-leaf-tree's proof that says "a second neighbor on the path would close a cycle"; the form the tree module's longest-path argument consumes.

Visited vertices along an inclusion

Walk.lean proves walkVertices monotone in the edge list. It is also monotone in the graph, which is what pulling a path down into a subgraph needs: the freshness clause of a path speaks about the subgraph's visited set, and that is the smaller one.

Edge deletion

Graph.deleteEdges is Mathlib's. These are the four transfer lemmas every deletion argument below reduces to.

theorem Graph.IsWalk.of_deleteEdges {α : Type u_1} {β : Type u_2} {G : Graph α β} {u v : α} {F : Set β} {W : List β} (h : (G.deleteEdges F).IsWalk u W v) : G.IsWalk u W v

Deleting edges never removes a vertex, so a walk in the deletion is a walk.

theorem Graph.IsWalk.notMem_of_deleteEdges {α : Type u_1} {β : Type u_2} {G : Graph α β} {u v : α} {f : β} {F : Set β} {W : List β} (h : (G.deleteEdges F).IsWalk u W v) (hf : f ∈ W) : f ∉ F

Conversely, a walk in the deletion could not have used a deleted name.

theorem Graph.IsPath.of_deleteEdges {α : Type u_1} {β : Type u_2} {G : Graph α β} {u v : α} {F : Set β} {W : List β} (h : (G.deleteEdges F).IsPath u W v) : G.IsPath u W v

theorem Graph.IsPath.deleteEdges {α : Type u_1} {β : Type u_2} {G : Graph α β} {u v : α} {F : Set β} {W : List β} (h : G.IsPath u W v) (hW : ∀ f ∈ W, f ∉ F) : (G.deleteEdges F).IsPath u W v

theorem Graph.IsPath.notMem_of_deleteEdges {α : Type u_1} {β : Type u_2} {G : Graph α β} {u v : α} {f : β} {F : Set β} {W : List β} (h : (G.deleteEdges F).IsPath u W v) (hf : f ∈ W) : f ∉ F

theorem Graph.Reaches.of_deleteEdges {α : Type u_1} {β : Type u_2} {G : Graph α β} {u v : α} {F : Set β} (h : (G.deleteEdges F).Reaches u v) : G.Reaches u v

theorem Graph.IsWalk.reaches_deleteEdges {α : Type u_1} {β : Type u_2} {G : Graph α β} {u v : α} {F : Set β} {W : List β} (h : G.IsWalk u W v) (hW : ∀ f ∈ W, f ∉ F) : (G.deleteEdges F).Reaches u v

Cycles

def Graph.IsCycleThrough {α : Type u_1} {β : Type u_2} (G : Graph α β) (e : β) (u v : α) (D : List β) : Prop

G.IsCycleThrough e u v D : the edge e links u to v, and D is a path from u back to v that does not use e. The cycle is e together with D; it is presented through e because that is the edge every question is asked about.

Equations

• G.IsCycleThrough e u v D = (G.IsLink e u v ∧ G.IsPath u D v ∧ e ∉ D)

def Graph.LiesOnCycle {α : Type u_1} {β : Type u_2} (G : Graph α β) (e : β) : Prop

G.LiesOnCycle e : the edge e lies on a cycle of G.

Equations

• G.LiesOnCycle e = ∃ (u : α) (v : α) (D : List β), G.IsCycleThrough e u v D

theorem Graph.IsCycleThrough.isLink {α : Type u_1} {β : Type u_2} {G : Graph α β} {u v : α} {e : β} {D : List β} (h : G.IsCycleThrough e u v D) : G.IsLink e u v

theorem Graph.IsCycleThrough.isPath {α : Type u_1} {β : Type u_2} {G : Graph α β} {u v : α} {e : β} {D : List β} (h : G.IsCycleThrough e u v D) : G.IsPath u D v

theorem Graph.IsCycleThrough.notMem {α : Type u_1} {β : Type u_2} {G : Graph α β} {u v : α} {e : β} {D : List β} (h : G.IsCycleThrough e u v D) : e ∉ D

theorem Graph.IsCycleThrough.liesOnCycle {α : Type u_1} {β : Type u_2} {G : Graph α β} {u v : α} {e : β} {D : List β} (h : G.IsCycleThrough e u v D) : G.LiesOnCycle e

theorem Graph.liesOnCycle_iff {α : Type u_1} {β : Type u_2} {G : Graph α β} {e : β} : G.LiesOnCycle e ↔ ∃ (u : α) (v : α) (D : List β), G.IsCycleThrough e u v D

theorem Graph.LiesOnCycle.edge_mem {α : Type u_1} {β : Type u_2} {G : Graph α β} {e : β} (h : G.LiesOnCycle e) : e ∈ G.edgeSet

An edge on a cycle is an edge of the graph. There is no converse hypothesis to carry around: Graph.IsLink already forces it.

theorem Graph.liesOnCycle_of_isLoopAt {α : Type u_1} {β : Type u_2} {G : Graph α β} {x : α} {e : β} (h : G.IsLoopAt e x) : G.LiesOnCycle e

A loop is a cycle of length one. The path back is the empty one, which trivially avoids the loop.

theorem Graph.liesOnCycle_of_parallel {α : Type u_1} {β : Type u_2} {G : Graph α β} {u v : α} {e f : β} (h : G.IsLink e u v) (h' : G.IsLink f u v) (hef : e ≠ f) : G.LiesOnCycle e

Two parallel edges are a cycle, on both of them. This is the length-two case, and the reason a walk names its edges.

theorem Graph.LiesOnCycle.mono {α : Type u_1} {β : Type u_2} {G H : Graph α β} {e : β} (hHG : H ≤ G) (h : H.LiesOnCycle e) : G.LiesOnCycle e

A cycle of a subgraph is a cycle of the graph.

The cycle criterion

The blueprint's lem:cycle-criterion. Both directions are one step each, once the deletion interface above is in place: forwards, the detour of the cycle is a walk that avoided e; backwards, a path in the deletion cannot have used e because e is not there.

theorem Graph.LiesOnCycle.deleteEdges_reaches {α : Type u_1} {β : Type u_2} {G : Graph α β} {u v : α} {e : β} (hl : G.IsLink e u v) (h : G.LiesOnCycle e) : (G.deleteEdges {e}).Reaches u v

An edge on a cycle is not needed to join its ends: the rest of the cycle still does.

The ends are given as an arbitrary pair u, v that e links, not as the pair the cycle was presented with — an edge has only two ends, so the two presentations agree up to a swap, and reachability is symmetric.

theorem Graph.LiesOnCycle.of_deleteEdges_reaches {α : Type u_1} {β : Type u_2} {G : Graph α β} {u v : α} {e : β} (hl : G.IsLink e u v) (h : (G.deleteEdges {e}).Reaches u v) : G.LiesOnCycle e

An edge whose deletion leaves its ends joined lies on a cycle. The route that survives is a walk of the deletion, hence contains a path of the deletion, and a path of the deletion cannot have used the name that was deleted.

theorem Graph.liesOnCycle_iff_deleteEdges_reaches {α : Type u_1} {β : Type u_2} {G : Graph α β} {u v : α} {e : β} (hl : G.IsLink e u v) : G.LiesOnCycle e ↔ (G.deleteEdges {e}).Reaches u v

The cycle criterion: an edge lies on a cycle if and only if deleting it does not disconnect its endpoints.

theorem Graph.IsWalk.reaches_deleteEdges_of_liesOnCycle {α : Type u_1} {β : Type u_2} {G : Graph α β} {u v : α} {e : β} {W : List β} (h : G.LiesOnCycle e) (hW : G.IsWalk u W v) : (G.deleteEdges {e}).Reaches u v

A walk reroutes around an edge that lies on a cycle: wherever it took e, it can go the long way round instead. Proved by induction along the walk rather than by splicing the detour into the edge list, so nothing has to be said about what the spliced list looks like.

theorem Graph.Connected.deleteEdges_singleton {α : Type u_1} {β : Type u_2} {G : Graph α β} {e : β} (hG : G.Connected) (h : G.LiesOnCycle e) : (G.deleteEdges {e}).Connected

Deleting an edge that lies on a cycle keeps the graph connected — the blueprint's "it is a tree: an edge of a cycle could be deleted", which is what makes a minimal connected spanning subgraph acyclic.

Chords

An edge from the source of a path to a vertex the path already visits closes a cycle. This is the shape in which acyclicity is used: it says a path cannot be extended backwards onto itself.

theorem Graph.IsPath.chord_liesOnCycle {α : Type u_1} {β : Type u_2} {G : Graph α β} {u v x : α} {e : β} {P : List β} (hP : G.IsPath u P v) (hl : G.IsLink e u x) (hoff : e ∉ P) (hx : x ∈ G.walkVertices u P) : G.LiesOnCycle e

A chord of a path lies on a cycle: the piece of the path from its source to the far end of the chord is a path avoiding the chord, so the chord closes it.

Acyclicity

def Graph.IsAcyclic {α : Type u_1} {β : Type u_2} (G : Graph α β) : Prop

G.IsAcyclic : no edge of G lies on a cycle. Stated over the edges of G because that is how a tree consumes it — every edge is a bridge — while Graph.IsAcyclic.not_liesOnCycle drops the membership hypothesis for the uses that do not have it to hand.

Equations

• G.IsAcyclic = ∀ ⦃e : β⦄, e ∈ G.edgeSet → ¬G.LiesOnCycle e

theorem Graph.IsAcyclic.not_liesOnCycle {α : Type u_1} {β : Type u_2} {G : Graph α β} (h : G.IsAcyclic) (e : β) : ¬G.LiesOnCycle e

Acyclicity with no membership hypothesis: an edge on a cycle would be an edge.

theorem Graph.isAcyclic_iff {α : Type u_1} {β : Type u_2} {G : Graph α β} : G.IsAcyclic ↔ ∀ (e : β), ¬G.LiesOnCycle e

theorem Graph.IsAcyclic.not_isLoopAt {α : Type u_1} {β : Type u_2} {G : Graph α β} (h : G.IsAcyclic) (e : β) (x : α) : ¬G.IsLoopAt e x

An acyclic graph has no loop. No hypothesis is needed anywhere else in this layer because of this: looplessness is a consequence of acyclicity, not a side condition on it.

theorem Graph.IsAcyclic.eq_of_isLink {α : Type u_1} {β : Type u_2} {G : Graph α β} {u v : α} {e f : β} (h : G.IsAcyclic) (hl : G.IsLink e u v) (hl' : G.IsLink f u v) : e = f

An acyclic graph has no parallel edges.

theorem Graph.IsAcyclic.anti {α : Type u_1} {β : Type u_2} {G H : Graph α β} (hHG : H ≤ G) (h : G.IsAcyclic) : H.IsAcyclic

A subgraph of an acyclic graph is acyclic.

theorem Graph.IsAcyclic.deleteEdges {α : Type u_1} {β : Type u_2} {G : Graph α β} (h : G.IsAcyclic) (F : Set β) : (G.deleteEdges F).IsAcyclic

theorem Graph.IsAcyclic.mem_of_isLink_of_mem_walkVertices {α : Type u_1} {β : Type u_2} {G : Graph α β} {u v x : α} {e : β} {P : List β} (hac : G.IsAcyclic) (hP : G.IsPath u P v) (hl : G.IsLink e u x) (hx : x ∈ G.walkVertices u P) : e ∈ P

In an acyclic graph, an edge at the source of a path whose far end the path visits is one of the path's own edges. This is the blueprint's "a second neighbor on the path would close a cycle" — the step that makes the end of a longest path a leaf, which is what the tree module runs on.

Bridges

def Graph.IsBridge {α : Type u_1} {β : Type u_2} (G : Graph α β) (e : β) : Prop

G.IsBridge e : an edge of G that lies on no cycle. Equivalently — and this is the form every use wants — an edge whose deletion separates its two ends (Graph.isBridge_iff_not_reaches).

Equations

• G.IsBridge e = (e ∈ G.edgeSet ∧ ¬G.LiesOnCycle e)

theorem Graph.IsBridge.edge_mem {α : Type u_1} {β : Type u_2} {G : Graph α β} {e : β} (h : G.IsBridge e) : e ∈ G.edgeSet

theorem Graph.IsBridge.not_liesOnCycle {α : Type u_1} {β : Type u_2} {G : Graph α β} {e : β} (h : G.IsBridge e) : ¬G.LiesOnCycle e

theorem Graph.IsBridge.not_reaches {α : Type u_1} {β : Type u_2} {G : Graph α β} {u v : α} {e : β} (h : G.IsBridge e) (hl : G.IsLink e u v) : ¬(G.deleteEdges {e}).Reaches u v

Deleting a bridge separates its ends.

theorem Graph.isBridge_of_not_reaches {α : Type u_1} {β : Type u_2} {G : Graph α β} {u v : α} {e : β} (hl : G.IsLink e u v) (h : ¬(G.deleteEdges {e}).Reaches u v) : G.IsBridge e

An edge whose deletion separates its ends is a bridge.

theorem Graph.isBridge_iff_not_reaches {α : Type u_1} {β : Type u_2} {G : Graph α β} {u v : α} {e : β} (hl : G.IsLink e u v) : G.IsBridge e ↔ ¬(G.deleteEdges {e}).Reaches u v

A bridge is exactly an edge whose deletion separates its ends — the cycle criterion, negated.

theorem Graph.IsBridge.not_isLoopAt {α : Type u_1} {β : Type u_2} {G : Graph α β} {e : β} (h : G.IsBridge e) (x : α) : ¬G.IsLoopAt e x

A bridge is never a loop: a loop is a cycle.

theorem Graph.isAcyclic_iff_forall_isBridge {α : Type u_1} {β : Type u_2} {G : Graph α β} : G.IsAcyclic ↔ ∀ e ∈ G.edgeSet, G.IsBridge e

A graph is acyclic exactly when every one of its edges is a bridge. This is the form the tree module wants acyclicity in: "it is a tree — an edge of a cycle could be deleted" reads backwards as "no edge can be deleted without separating its ends".

theorem Graph.IsAcyclic.isBridge {α : Type u_1} {β : Type u_2} {G : Graph α β} {e : β} (h : G.IsAcyclic) (he : e ∈ G.edgeSet) : G.IsBridge e