Lax17.TerminalConnectivity

Terminal element connectivity and split-off operations

concepts/Lax17/TerminalConnectivity.lean · lax-17

definition

Loading review…

Concept map

Proven claimDefinitionThis conceptRelated conceptA → B: B builds on A

Definition

A finite edge-indexed graph is a loopless undirected multigraph whose parallel edge copies retain distinct names. Terminal element connectivity counts a separator made from nonterminal vertices and edge copies. Deletion removes one named edge; contraction identifies its endpoints and discards resulting loops; splitting off two edges at a centre replaces them by an edge between their other endpoints, discarding that edge when it would be a loop.

These definitions are the natural multigraph language for the Hind–Oellermann and Mader reductions used in the grid-minor proof.

Lean source view on GitHub

1	import Mathlib.Data.Finset.Sym
2	import Mathlib.Data.Fintype.Sum
3
4	/-!
5	---
6	title: Terminal element connectivity and split-off operations
7	type: definition
8	---
9	A finite edge-indexed graph is a loopless undirected multigraph whose parallel
10	edge copies retain distinct names. Terminal element connectivity counts a
11	separator made from nonterminal vertices and edge copies. Deletion removes
12	one named edge; contraction identifies its endpoints and discards resulting
13	loops; splitting off two edges at a centre replaces them by an edge between
14	their other endpoints, discarding that edge when it would be a loop.
15
16	These definitions are the natural multigraph language for the
17	Hind--Oellermann and Mader reductions used in the grid-minor proof.
18	-/
19
20	namespace Lax17.TerminalConnectivity
21
22	universe u v
23
24	/-- A finite loopless undirected multigraph with named edge copies. -/
25	structure EdgeIndexedGraph (V : Type u) where
26	Edge : Type
27	[edgeFintype : Fintype Edge]
28	[edgeDecidableEq : DecidableEq Edge]
29	left : Edge → V
30	right : Edge → V
31	end_ne : ∀ e : Edge, left e ≠ right e
32
33	namespace EdgeIndexedGraph
34
35	instance {V : Type u} (H : EdgeIndexedGraph V) : Fintype H.Edge :=
36	H.edgeFintype
37
38	instance {V : Type u} (H : EdgeIndexedGraph V) : DecidableEq H.Edge :=
39	H.edgeDecidableEq
40
41	/-- Named edge copies incident with `x`. -/
42	def incidentEdges {V : Type u} [Fintype V] [DecidableEq V]
43	(H : EdgeIndexedGraph V) (x : V) : Finset H.Edge :=
44	Finset.univ.filter fun e => H.left e = x ∨ H.right e = x
45
46	/-- Degree, counting parallel copies separately. -/
47	def degree {V : Type u} [Fintype V] [DecidableEq V]
48	(H : EdgeIndexedGraph V) (x : V) : ℕ :=
49	(H.incidentEdges x).card
50
51	/-- A named edge has exactly one endpoint in `S`. -/
52	def Crosses {V : Type u} [DecidableEq V]
53	(H : EdgeIndexedGraph V) (S : Finset V) (e : H.Edge) : Prop :=
54	(H.left e ∈ S ∧ H.right e ∉ S) ∨
55	(H.right e ∈ S ∧ H.left e ∉ S)
56
57	/-- The named edge boundary of `S`. -/
58	noncomputable def boundary {V : Type u} [Fintype V] [DecidableEq V]
59	(H : EdgeIndexedGraph V) (S : Finset V) : Finset H.Edge :=
60	@Finset.filter H.Edge (H.Crosses S) (Classical.decPred _) Finset.univ
61
62	/-- Boundary edges whose endpoints survive deletion of `removed`. -/
63	noncomputable def availableBoundary
64	{V : Type u} [Fintype V] [DecidableEq V]
65	(H : EdgeIndexedGraph V) (removed S : Finset V) : Finset H.Edge :=
66	(H.boundary S).filter fun e =>
67	H.left e ∉ removed ∧ H.right e ∉ removed
68
69	/-- A terminal-separating cut made from nonterminal vertices and named edge
70	copies. -/
71	structure ElementCut
72	{V : Type u} [Fintype V] [DecidableEq V]
73	(H : EdgeIndexedGraph V) (terminals : Finset V) (a b : V) where
74	removedVertices : Finset V
75	removedVertices_nonterminal : Disjoint removedVertices terminals
76	removedEdges : Finset H.Edge
77	side : Finset V
78	source_mem : a ∈ side
79	target_not_mem : b ∉ side
80	side_disjoint_removed : Disjoint side removedVertices
81	crossing_removed :
82	∀ e : H.Edge,
83	H.left e ∉ removedVertices →
84	H.right e ∉ removedVertices →
85	H.Crosses side e →
86	e ∈ removedEdges
87
88	namespace ElementCut
89
90	/-- Number of removed vertices and named edge copies. -/
91	def order
92	{V : Type u} [Fintype V] [DecidableEq V]
93	{H : EdgeIndexedGraph V} {terminals : Finset V} {a b : V}
94	(C : ElementCut H terminals a b) : ℕ :=
95	C.removedVertices.card + C.removedEdges.card
96
97	end ElementCut
98
99	/-- Every two distinct terminals need at least `k` nonterminal vertices and
100	edge copies to separate them. -/
101	def TerminalElementConnectedAtLeast
102	{V : Type u} [Fintype V] [DecidableEq V]
103	(H : EdgeIndexedGraph V) (terminals : Finset V) (k : ℕ) : Prop :=
104	∀ ⦃a : V⦄, a ∈ terminals →
105	∀ ⦃b : V⦄, b ∈ terminals → a ≠ b →
106	∀ removed side : Finset V,
107	Disjoint removed terminals →
108	a ∈ side → b ∉ side → Disjoint side removed →
109	k ≤ removed.card + (H.availableBoundary removed side).card
110
111	/-- Delete one named edge copy. -/
112	def deleteEdge {V : Type u} (H : EdgeIndexedGraph V) (e₀ : H.Edge) :
113	EdgeIndexedGraph V where
114	Edge := {e : H.Edge // e ≠ e₀}
115	left e := H.left e.1
116	right e := H.right e.1
117	end_ne e := H.end_ne e.1
118
119	/-- A concrete model of contracting `e₀`. The vertex map has precisely the
120	contracted endpoint pair as its only nontrivial fibre, and the target edges
121	are exactly the surviving non-loop edge copies. -/
122	structure IsContraction
123	{V : Type u} {W : Type v} [DecidableEq W]
124	(H : EdgeIndexedGraph V) (e₀ : H.Edge)
125	(K : EdgeIndexedGraph W) (mapVertex : V → W) where
126	vertex_surjective : Function.Surjective mapVertex
127	endpoints_identified :
128	mapVertex (H.left e₀) = mapVertex (H.right e₀)
129	fibres :
130	∀ ⦃x y : V⦄, mapVertex x = mapVertex y →
131	x = y ∨
132	(x = H.left e₀ ∧ y = H.right e₀) ∨
133	(x = H.right e₀ ∧ y = H.left e₀)
134	edgeEquiv :
135	{e : H.Edge //
136	e ≠ e₀ ∧ mapVertex (H.left e) ≠ mapVertex (H.right e)} ≃ K.Edge
137	edge_endpoints :
138	∀ e,
139	(K.left (edgeEquiv e) = mapVertex (H.left e.1) ∧
140	K.right (edgeEquiv e) = mapVertex (H.right e.1)) ∨
141	(K.left (edgeEquiv e) = mapVertex (H.right e.1) ∧
142	K.right (edgeEquiv e) = mapVertex (H.left e.1))
143
144	/-- Image of the terminal set under a contraction map. -/
145	def terminalImage {V : Type u} {W : Type v} [DecidableEq W]
146	(mapVertex : V → W) (terminals : Finset V) : Finset W :=
147	terminals.image mapVertex
148
149	/-- Two distinct named edges incident with `s`, with their other endpoints. -/
150	structure SplitPair {V : Type u} (H : EdgeIndexedGraph V) (s : V) where
151	first : H.Edge
152	second : H.Edge
153	edge_ne : first ≠ second
154	firstOther : V
155	secondOther : V
156	first_ends :
157	(H.left first = s ∧ H.right first = firstOther) ∨
158	(H.right first = s ∧ H.left first = firstOther)
159	second_ends :
160	(H.left second = s ∧ H.right second = secondOther) ∨
161	(H.right second = s ∧ H.left second = secondOther)
162
163	/-- Edge names surviving or created by a split-off. The right summand is
164	inhabited exactly when the newly created edge is not a loop. -/
165	def SplitEdge
166	{V : Type u} [DecidableEq V] {H : EdgeIndexedGraph V} {s : V}
167	(p : H.SplitPair s) : Type :=
168	{e : H.Edge // e ≠ p.first ∧ e ≠ p.second} ⊕
169	{_unit : Unit // p.firstOther ≠ p.secondOther}
170
171	noncomputable instance splitEdgeFintype
172	{V : Type u} [DecidableEq V] {H : EdgeIndexedGraph V} {s : V}
173	(p : H.SplitPair s) : Fintype (SplitEdge p) :=
174	letI : Fintype {e : H.Edge // e ≠ p.first ∧ e ≠ p.second} :=
175	Fintype.ofInjective Subtype.val Subtype.val_injective
176	letI : Fintype {_unit : Unit // p.firstOther ≠ p.secondOther} :=
177	Fintype.ofInjective Subtype.val Subtype.val_injective
178	inferInstanceAs
179	(Fintype
180	({e : H.Edge // e ≠ p.first ∧ e ≠ p.second} ⊕
181	{_unit : Unit // p.firstOther ≠ p.secondOther}))
182
183	noncomputable instance splitEdgeDecidableEq
184	{V : Type u} [DecidableEq V] {H : EdgeIndexedGraph V} {s : V}
185	(p : H.SplitPair s) : DecidableEq (SplitEdge p) :=
186	Classical.decEq (SplitEdge p)
187
188	/-- Split off a pair of edges at `s`, discarding a newly created loop. -/
189	noncomputable def splitOff {V : Type u} [DecidableEq V]
190	(H : EdgeIndexedGraph V) {s : V}
191	(p : H.SplitPair s) : EdgeIndexedGraph V where
192	Edge := SplitEdge p
193	left
194	\| Sum.inl e => H.left e.1
195	\| Sum.inr _ => p.firstOther
196	right
197	\| Sum.inl e => H.right e.1
198	\| Sum.inr _ => p.secondOther
199	end_ne
200	\| Sum.inl e => H.end_ne e.1
201	\| Sum.inr e => e.2
202
203	/-- `u` and `v` cannot be separated by fewer than `k` edge copies. -/
204	def PairEdgeConnectedAtLeast
205	{V : Type u} [Fintype V] [DecidableEq V]
206	(H : EdgeIndexedGraph V) (u v : V) (k : ℕ) : Prop :=
207	∀ S : Finset V, u ∈ S → v ∉ S → k ≤ (H.boundary S).card
208
209	/-- Splitting `p` preserves every local edge-connectivity value away from its
210	centre. -/
211	def IsMaderAdmissible
212	{V : Type u} [Fintype V] [DecidableEq V]
213	(H : EdgeIndexedGraph V) {s : V} (p : H.SplitPair s) : Prop :=
214	∀ u v : V, u ≠ s → v ≠ s → u ≠ v → ∀ k : ℕ,
215	H.PairEdgeConnectedAtLeast u v k ↔
216	(H.splitOff p).PairEdgeConnectedAtLeast u v k
217
218	/-- A named edge is the whole boundary of some vertex set. -/
219	def IsNamedCutEdge {V : Type u} [Fintype V] [DecidableEq V]
220	(H : EdgeIndexedGraph V) (e : H.Edge) : Prop :=
221	∃ S : Finset V, H.boundary S = {e}
222
223	/-- No edge incident with `s` is a named cut edge. -/
224	def NoIncidentCutEdge {V : Type u} [Fintype V] [DecidableEq V]
225	(H : EdgeIndexedGraph V) (s : V) : Prop :=
226	∀ e ∈ H.incidentEdges s, ¬ H.IsNamedCutEdge e
227
228	/-- A simple path in an edge-indexed multigraph. -/
229	structure Path {V : Type u} [DecidableEq V]
230	(H : EdgeIndexedGraph V) (source target : V) where
231	length : ℕ
232	vertex : Fin (length + 1) → V
233	edge : Fin length → H.Edge
234	source_eq : vertex 0 = source
235	target_eq : vertex (Fin.last length) = target
236	edge_ends :
237	∀ i : Fin length,
238	(H.left (edge i) = vertex i.castSucc ∧
239	H.right (edge i) = vertex i.succ) ∨
240	(H.right (edge i) = vertex i.castSucc ∧
241	H.left (edge i) = vertex i.succ)
242	vertex_injective : Function.Injective vertex
243
244	namespace Path
245
246	/-- The internal vertices of an edge-indexed path. -/
247	def internalVertices
248	{V : Type u} [DecidableEq V] {H : EdgeIndexedGraph V}
249	{source target : V} (P : Path H source target) : Finset V :=
250	((Finset.univ.image P.vertex).erase source).erase target
251
252	/-- The named edge copies used by an edge-indexed path. -/
253	def edgeSet
254	{V : Type u} [DecidableEq V] {H : EdgeIndexedGraph V}
255	{source target : V} (P : Path H source target) : Finset H.Edge :=
256	Finset.univ.image P.edge
257
258	end Path
259
260	/-- `k` paths from `a` to `b` sharing neither internal vertices nor named
261	edge copies. -/
262	structure ElementLinkage
263	{V : Type u} [DecidableEq V]
264	(H : EdgeIndexedGraph V) (a b : V) (k : ℕ) where
265	path : Fin k → Path H a b
266	internal_disjoint :
267	Pairwise fun i j =>
268	Disjoint (path i).internalVertices (path j).internalVertices
269	edge_disjoint :
270	Pairwise fun i j =>
271	Disjoint (path i).edgeSet (path j).edgeSet
272
273	end EdgeIndexedGraph
274
275	end Lax17.TerminalConnectivity
276

Builds on

none

Used by

From Mathlib

Community review

Discussion

Ask a question or add context. Endorsements and structured flags are kept in the review panel above; your ORCID profile must share a public name.

0 comments

Loading discussion…

Lax Lean Archive

Terminal element connectivity and split-off operations

Flags

Flag this concept