Documentation

TauCeti.Combinatorics.SimpleGraph.Connectivity.Ear.Open

Open ear decompositions and 2-vertex-connectivity #

Whitney's theorem (1932) characterizes 2-vertex-connected finite simple graphs as those admitting an open ear decomposition: starting from a cycle, one repeatedly adjoins paths between two distinct vertices already present whose internal vertices and edges are new.

This file proves both directions at their natural generality:

Because Graph.IsVertexConnected G 2 is an abbrev for G.toSimpleGraph.IsVertexConnected 2, the equivalence applies directly to the underlying simple graph of any multigraph with finitely many actual vertices ([Finite V(G)]), regardless of loops or parallel edges.

Main results #

Implementation notes #

In the soundness direction, deleting a set s of fewer than two vertices leaves s having encard ≤ 1 (Set.encard_le_one_iff). On an open ear p from u to v, splitting p at any undeleted internal vertex w yields two internally disjoint subwalks to u and v, at least one of which avoids s and lifts via SimpleGraph.Walk.reachable_induce_coe_of_mem_support. In the completeness direction, Finite G.Subgraph (from [Finite V]) gives WellFoundedGT G.Subgraph, so producing an open ear decomposition of ⊤ with the same initial subgraph along Ear.lt_adjoin requires no auxiliary edge-count measure or [DecidableEq V] assumption.

References #

Soundness: open ears preserve 2-vertex-connectivity #

source
theorem SimpleGraph.Ear.isVertexConnected_two_adjoin {V : Type u} {G : SimpleGraph V} {H : G.Subgraph} (hH : H.coe.IsVertexConnected 2) {e : G.Ear H} (he : e.kind = EarKind.open) :
e.adjoin.coe.IsVertexConnected 2

Adjoining an open ear to a 2-vertex-connected subgraph preserves 2-vertex-connectivity, with no finiteness assumption.

source
theorem SimpleGraph.EarStart.IsCycle.isVertexConnected_two {V : Type u} {G : SimpleGraph V} {H : G.Subgraph} {s : G.EarStart H} (hs : s.IsCycle) :
H.coe.IsVertexConnected 2

A cycle initial witness yields a 2-vertex-connected initial subgraph.

source
theorem SimpleGraph.EarDecomposition.IsOpen.isVertexConnected_two_initial {V : Type u} {G : SimpleGraph V} {H : G.Subgraph} {d : G.EarDecomposition H} (hd : d.IsOpen) :
d.initial.coe.IsVertexConnected 2

The initial subgraph of an open ear decomposition is 2-vertex-connected, with no finiteness assumption.

source
theorem SimpleGraph.EarDecomposition.IsOpen.isVertexConnected_two_subgraphAfter {V : Type u} {G : SimpleGraph V} {H : G.Subgraph} {d : G.EarDecomposition H} (hd : d.IsOpen) (k : Fin (d.length + 1)) :
(d.subgraphAfter k).coe.IsVertexConnected 2

Every prefix subgraph of an open ear decomposition is 2-vertex-connected, with no finiteness assumption.

source
theorem SimpleGraph.EarDecomposition.IsOpen.isVertexConnected_two_final {V : Type u} {G : SimpleGraph V} {H : G.Subgraph} {d : G.EarDecomposition H} (hd : d.IsOpen) :
H.coe.IsVertexConnected 2

The final subgraph of an open ear decomposition is 2-vertex-connected, with no finiteness assumption.

source
theorem SimpleGraph.EarDecomposition.IsOpen.isVertexConnected_two {V : Type u} {G : SimpleGraph V} {d : G.EarDecomposition ⊤} (hd : d.IsOpen) :
G.IsVertexConnected 2

A simple graph admitting an open ear decomposition of ⊤ is 2-vertex-connected, with no finiteness assumption.

Completeness: constructing open ears and open ear decompositions #

source
theorem SimpleGraph.IsVertexConnected.exists_open_ear {V : Type u} {G : SimpleGraph V} [Finite V] (hG : G.IsVertexConnected 2) {H : G.Subgraph} (hH : H ≠ ⊤) (hverts : H.verts.Nontrivial) :
∃ (e : G.Ear H), e.kind = EarKind.open

Single-step open ear existence. In a 2-vertex-connected simple graph on a finite vertex type, every proper subgraph H ≠ ⊤ with at least two vertices admits an open ear.

source
theorem SimpleGraph.IsVertexConnected.exists_isOpen_earDecomposition_of_earDecomposition {V : Type u} {G : SimpleGraph V} [Finite V] (hG : G.IsVertexConnected 2) {H : G.Subgraph} (d₀ : G.EarDecomposition H) (hd₀ : d₀.IsOpen) :
∃ (d : G.EarDecomposition ⊤), d.IsOpen ∧ d.initial = d₀.initial

Given an open ear decomposition of a subgraph H in a finite 2-vertex-connected simple graph, there exists an open ear decomposition of ⊤ with the same initial subgraph.

source
theorem SimpleGraph.IsVertexConnected.exists_isOpen_earDecomposition_initial_eq {V : Type u} {G : SimpleGraph V} [Finite V] (hG : G.IsVertexConnected 2) {u : V} (c : G.Walk u u) (hc : c.IsCycle) :
∃ (d : G.EarDecomposition ⊤), d.IsOpen ∧ d.initial = c.toSubgraph

Whitney's theorem with prescribed initial cycle. For any cycle c in a 2-vertex-connected simple graph on a finite vertex type, there is an open ear decomposition of ⊤ whose initial subgraph is c.toSubgraph.

source
theorem SimpleGraph.IsVertexConnected.exists_isOpen_earDecomposition_mem_edgeSet_initial {V : Type u} {G : SimpleGraph V} [Finite V] (hG : G.IsVertexConnected 2) {e : Sym2 V} (he : e ∈ G.edgeSet) :
∃ (d : G.EarDecomposition ⊤), d.IsOpen ∧ e ∈ d.initial.edgeSet

Prescribed-edge open ear decomposition. Every edge of a finite 2-vertex-connected simple graph belongs to the initial cycle of some open ear decomposition of ⊤.

source
theorem SimpleGraph.Adj.exists_isOpen_earDecomposition_adj_initial {V : Type u} {G : SimpleGraph V} [Finite V] {s t : V} (hadj : G.Adj s t) (hG : G.IsVertexConnected 2) :
∃ (d : G.EarDecomposition ⊤), d.IsOpen ∧ d.initial.Adj s t

Adjacency form of IsVertexConnected.exists_isOpen_earDecomposition_mem_edgeSet_initial.

source
theorem SimpleGraph.isVertexConnected_two_iff_exists_isOpen_earDecomposition {V : Type u} {G : SimpleGraph V} [Finite V] :
G.IsVertexConnected 2 ↔ ∃ (d : G.EarDecomposition ⊤), d.IsOpen

Whitney's open ear characterization of 2-vertex-connectivity. A simple graph on a finite vertex type is 2-vertex-connected if and only if it admits an open ear decomposition of ⊤. No separate cardinality bound on V is required: both sides entail at least three vertices.