Lax17.TreeOfSets

Strong tree-of-sets systems

concepts/Lax17/TreeOfSets.lean · lax-17

definition

Loading review…

Concept map

Proven claimDefinitionThis conceptRelated conceptA → B: B builds on A

Definition

A tree-of-sets system replaces the linear order of a path-of-sets system by a subcubic tree. Its vertices index disjoint connected clusters, and each tree edge has a linkage between equal-size interfaces in its endpoint clusters. A strong system makes every interface well-linked and every pair of interfaces incident with one cluster mutually linked inside that cluster.

Lean source view on GitHub

1	import Mathlib.Combinatorics.SimpleGraph.Acyclic
2	import Lax17.Degree
3	import Lax17.PathOfSets
4
5	/-!
6	---
7	title: Strong tree-of-sets systems
8	type: definition
9	---
10	A tree-of-sets system replaces the linear order of a path-of-sets system by a
11	subcubic tree. Its vertices index disjoint connected clusters, and each
12	tree edge has a linkage between equal-size interfaces in its endpoint
13	clusters. A strong system makes every interface well-linked and every pair of
14	interfaces incident with one cluster mutually linked inside that cluster.
15	-/
16
17	namespace Lax17.TreeOfSets
18
19	universe u
20
21	open Lax17.Degree
22	open Lax17.Linkedness
23	open Lax17.PathOfSets
24	open Lax17.Paths
25
26	/-- A subcubic tree-of-sets system with `m` clusters and width `w`. -/
27	structure System {V : Type u} [DecidableEq V]
28	(G : SimpleGraph V) (m w : ℕ) where
29	clusterCount_pos : 0 < m
30	width_pos : 0 < w
31	metaTree : SimpleGraph (Fin m)
32	meta_isTree : metaTree.IsTree
33	meta_subcubic : MaximumAtMost metaTree 3
34	cluster : Fin m → Finset V
35	cluster_connected : ∀ i : Fin m, IsCluster G (cluster i)
36	cluster_disjoint :
37	∀ ⦃i j : Fin m⦄, i ≠ j → Disjoint (cluster i) (cluster j)
38	interface :
39	(i j : Fin m) → metaTree.Adj i j → Finset V
40	interface_subset :
41	∀ (i j : Fin m) (hij : metaTree.Adj i j),
42	interface i j hij ⊆ cluster i
43	interface_card :
44	∀ (i j : Fin m) (hij : metaTree.Adj i j),
45	(interface i j hij).card = w
46	incident_interfaces_disjoint :
47	∀ {i j k : Fin m} (hij : metaTree.Adj i j)
48	(hik : metaTree.Adj i k),
49	j ≠ k → Disjoint (interface i j hij) (interface i k hik)
50	connector :
51	∀ (i j : Fin m) (hij : metaTree.Adj i j),
52	VertexLinkage G (interface i j hij)
53	(interface j i (metaTree.symm hij)) w
54	connector_avoids_clusters :
55	∀ (i j : Fin m) (hij : metaTree.Adj i j)
56	(r : Fin m) (a : Fin w),
57	((connector i j hij).path a).InternallyAvoids (cluster r)
58	connectors_disjoint :
59	∀ (i j : Fin m) (hij : metaTree.Adj i j)
60	(p q : Fin m) (hpq : metaTree.Adj p q),
61	s(i, j) ≠ s(p, q) →
62	∀ a b : Fin w,
63	Disjoint ((connector i j hij).path a).vertices
64	((connector p q hpq).path b).vertices
65
66	/-- A strong tree-of-sets system. -/
67	structure StrongSystem {V : Type u} [DecidableEq V]
68	(G : SimpleGraph V) (m w : ℕ) extends System G m w where
69	interface_well_linked :
70	∀ (i j : Fin m) (hij : metaTree.Adj i j),
71	NodeWellLinkedIn G (cluster i) (interface i j hij)
72	incident_interfaces_linked :
73	∀ {i j k : Fin m} (hij : metaTree.Adj i j)
74	(hik : metaTree.Adj i k),
75	j ≠ k →
76	NodeLinkedIn G (cluster i)
77	(interface i j hij) (interface i k hik)
78
79	/-- The meta-tree contains an ordered simple path with `ℓ` vertices. -/
80	def HasMetaPath {V : Type u} [DecidableEq V]
81	{G : SimpleGraph V} {m w : ℕ}
82	(T : StrongSystem G m w) (ℓ : ℕ) : Prop :=
83	∃ order : Fin ℓ → Fin m,
84	Function.Injective order ∧
85	∀ (i : Fin ℓ) (hi : i.1 + 1 < ℓ),
86	T.metaTree.Adj (order i) (order ⟨i.1 + 1, hi⟩)
87
88	end Lax17.TreeOfSets
89

Builds on

Used by

From Mathlib

Mathlib.Combinatorics.SimpleGraph.Acyclic

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

Strong tree-of-sets systems

Flags

Flag this concept