Partial tree decompositions #
A PartialDecomposition H U is a tree decomposition of the subgraph of H
induced on the finset U, carried on the same vertex type V: bags are
finsets of V contained in U, and the coverage/coherence axioms are asserted
only for vertices of U.
Why this notion exists #
TreewidthGonality/Treewidth/TreeDecomposition.lean's TreeDecomposition H demands
cover_vertex : ∀ v : V, ∃ t, v ∈ bag t — every vertex of the ambient type.
The Bellenbaum--Diestel induction for Seymour--Thomas duality builds a decomposition of G
from a root bag X together with decompositions of the subgraphs
G[C ∪ X], C a component of G − X. Those pieces are not
TreeDecompositions of anything on V, and making them so by moving to the
subtype ↥(↑(C ∪ X) : Set V) would push every statement downstream (bags,
cardinalities, Bramble members, the separator of the Menger-free Lemma 2)
through a coercion tower that changes at each level of the recursion. Hence
this relative notion, with U = Finset.univ recovering the absolute one via
toTreeDecomposition.
Gluing #
The paper glues the per-component decompositions by identifying their
X-nodes. Here they are instead joined pairwise, keeping both copies of
the X-node (they carry the same bag X, so duplicating costs nothing) and
adding a bridge between them; SeymourThomasInduction.lean folds that binary
join over the components one at a time. The payoff is that the joined tree
is (T₁ ⊕g T₂) ⊔ SimpleGraph.edge _ _, which is exactly the shape mathlib
supports: SimpleGraph.Connected.sum_sup_edge gives connectivity and
SimpleGraph.isTree_iff_connected_and_card converts an edge count into
IsTree, so acyclicity is never proved directly.
Contents #
PartialDecomposition,width,toTreeDecomposition;single— the one-bag decomposition ofHonU = X;connected_induce_inl_image/..._inr_image— transport of induced connectivity along the two summand inclusions;join— the binary gluing along a common root bag.
A partial tree decomposition: a tree decomposition of the subgraph of
H induced on U, stated on the ambient vertex type V.
bag_subset is what makes the notion relative; cover_vertex, cover_edge
and coherent are the three usual axioms restricted to U. For v ∉ U no
bag contains v (by bag_subset), which is why coherent may be — and must
be — asserted only on U: SimpleGraph.Connected bundles Nonempty.
- Node : Type
The nodes of the decomposition tree.
- nodeDecidableEq : DecidableEq self.Node
- tree : SimpleGraph self.Node
The decomposition tree.
treereally is a tree.The bag of vertices at each node.
Every bag lies inside
U.Every vertex of
Uappears in some bag.- cover_edge (v : V) : v ∈ U → ∀ w ∈ U, H.Adj v w → ∃ (t : self.Node), v ∈ self.bag t ∧ w ∈ self.bag t
Every edge of
HinsideUhas both endpoints in a common bag. - coherent (v : V) : v ∈ U → (SimpleGraph.induce {t : self.Node | v ∈ self.bag t} self.tree).Connected
The nodes containing a fixed vertex of
Uform a connected subtree.
Instances For
The width of a partial decomposition, defined exactly as for
TreeDecomposition.
Instances For
Every bag has at most width + 1 vertices.
A partial decomposition on all of V is a tree decomposition.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The width of a decomposition of all of V, as a TreeDecomposition, is
the width of the partial decomposition.
The one-bag decomposition #
The one-bag partial decomposition: a single node carrying the bag X,
a decomposition of H on U = X.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Transport of induced connectivity along the summand inclusions #
join's coherence proof needs to know that a connected set of nodes on one
side stays connected after the two trees are summed and bridged. There is no
mathlib lemma for this; it is a walk map (SimpleGraph.Walk.map along
SimpleGraph.Embedding.sumInl, then Walk.mapLe, then Walk.induce).
A connected node set of the left summand stays connected in any graph above the sum.
A connected node set of the right summand stays connected in any graph above the sum.
The binary join #
The tree of join: the two trees side by side, plus a bridge between the
two root nodes.
Equations
- Utilities.Treewidth.PartialDecomposition.joinTree T₁ T₂ r₁ r₂ = (T₁ ⊕g T₂) ⊔ SimpleGraph.edge (Sum.inl r₁) (Sum.inr r₂)
Instances For
joinTree of two trees is a tree.
Discharge plan: SimpleGraph.isTree_iff_connected_and_card. Connectivity is
SimpleGraph.Connected.sum_sup_edge. For the edge count, the two edge sets are
disjoint (Sum.inl r₁ and Sum.inr r₂ are non-adjacent in the sum by
SimpleGraph.not_adj_sum_inl_inr), SimpleGraph.edgeSetSumEquiv splits the
sum's edge set, and SimpleGraph.IsTree.card_edgeFinset gives
|Eᵢ| + 1 = |Nᵢ|, so (|N₁| - 1) + (|N₂| - 1) + 1 + 1 = |N₁ ⊕ N₂|.
Acyclicity is never proved directly.
The binary join. Two partial decompositions sharing the bag X at a
designated node are glued into a partial decomposition of the union, again with
bag X at a designated node (Sum.inl r₁).
hcap says the two ground sets meet only inside X, and hsep says H has no
edge between U₁ \ X and U₂ \ X; for the components of H − X both hold.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The two-bag decomposition. Two nodes joined by an edge, carrying the
bags X and Y; a decomposition of H on X ∪ Y whenever every edge of H
inside X ∪ Y has both ends in X or both ends in Y.
This is the decomposition the paper uses in the branch where 𝔅 ∪ {C} fails to
be a bramble (X and Y := V(C) ∪ N(C)).
Equations
- One or more equations did not get rendered due to their size.
Instances For
Every bag of pairDecomp is X or Y.
Every bag of a join is a bag of one of the two pieces.