Brambles and the bramble number

A bramble of a simple graph H is a collection of connected vertex sets that pairwise touch: any two of them have connected union. A hitting set meets every member, and the order of the bramble is the least size of a hitting set. Seymour--Thomas duality says the largest order of a bramble is treewidth H + 1; the half of that used here is proved in TreewidthGonality/Treewidth/SeymourThomas.lean.

Conventions

Connectivity of a vertex set is (H.induce (↑S : Set V)).Connected, as fixed in the module docstring of TreewidthGonality/Treewidth/TreeDecomposition.lean. Since SimpleGraph.Connected bundles Nonempty, the connected_mem field already forces every member of a bramble to be nonempty (Bramble.nonempty_of_mem), so there is no separate nonemptiness field.

order is an sInf over ℕ; hittingSetCards_nonempty (all of V is a hitting set) is what makes it meaningful rather than the sInf ∅ = 0 default.

theorem Utilities.Treewidth.exists_adj_across_of_walk {W : Type u_1} {K : SimpleGraph W} {a b : W} (S : Set W) (p : K.Walk a b) (ha : a ∈ S) (hb : b ∉ S) : ∃ v ∈ S, ∃ w ∉ S, K.Adj v w

First-crossing lemma. A walk that starts inside S and ends outside it uses an edge from S to its complement. This is the same induction as the private walk_has_edge_across_cut of Utilities/Foundations/UnderlyingSimpleGraph.lean, restated here (that one is not exported) and used both by Bramble.exists_inter_or_adj and by TreewidthGonality/Gonality/BrambleGonality.lean.

structure Utilities.Treewidth.Bramble {V : Type u} [DecidableEq V] (H : SimpleGraph V) : Type u

A bramble of H: a finite family of vertex sets, each inducing a connected subgraph, any two of which have connected union ("they touch").

Taking B = B' in touching recovers connected_mem, so the latter is redundant; it is kept because it is the field consumers use and because it makes the definition read the way the literature states it.

• members : Finset (Finset V)

  The members of the bramble.

• connected_mem (B : Finset V) : B ∈ self.members → (SimpleGraph.induce (↑B) H).Connected

  Each member induces a connected subgraph (in particular is nonempty).

• touching (B : Finset V) : B ∈ self.members → ∀ B' ∈ self.members, (SimpleGraph.induce (↑(B ∪ B')) H).Connected

  Any two members touch: their union induces a connected subgraph.

theorem Utilities.Treewidth.Bramble.nonempty_of_mem {V : Type u} [DecidableEq V] {H : SimpleGraph V} (𝔅 : Bramble H) {B : Finset V} (hB : B ∈ 𝔅.members) : B.Nonempty

Members of a bramble are nonempty: SimpleGraph.Connected bundles Nonempty.

def Utilities.Treewidth.Bramble.IsHittingSet {V : Type u} [DecidableEq V] {H : SimpleGraph V} (𝔅 : Bramble H) (S : Finset V) : Prop

A hitting set of a bramble meets every member.

Equations

• 𝔅.IsHittingSet S = ∀ B ∈ 𝔅.members, (B ∩ S).Nonempty

def Utilities.Treewidth.Bramble.hittingSetCards {V : Type u} [DecidableEq V] {H : SimpleGraph V} (𝔅 : Bramble H) : Set ℕ

The sizes of the hitting sets of 𝔅.

Equations

• 𝔅.hittingSetCards = {n : ℕ | ∃ (S : Finset V), 𝔅.IsHittingSet S ∧ S.card = n}

noncomputable def Utilities.Treewidth.Bramble.order {V : Type u} [DecidableEq V] {H : SimpleGraph V} (𝔅 : Bramble H) : ℕ

The order of a bramble: the least size of a hitting set.

Equations

• 𝔅.order = sInf 𝔅.hittingSetCards

theorem Utilities.Treewidth.Bramble.order_le_card_of_isHittingSet {V : Type u} [DecidableEq V] {H : SimpleGraph V} (𝔅 : Bramble H) {S : Finset V} (hS : 𝔅.IsHittingSet S) : 𝔅.order ≤ S.card

Any hitting set bounds the order.

def Utilities.Treewidth.Bramble.restrict {V : Type u} [DecidableEq V] {H : SimpleGraph V} (𝔅 : Bramble H) (M : Finset (Finset V)) (hM : M ⊆ 𝔅.members) : Bramble H

Restricting a bramble to a subfamily of its members is again a bramble.

Equations

• 𝔅.restrict M hM = { members := M, connected_mem := ⋯, touching := ⋯ }

@[simp]

theorem Utilities.Treewidth.Bramble.restrict_members {V : Type u} [DecidableEq V] {H : SimpleGraph V} (𝔅 : Bramble H) (M : Finset (Finset V)) (hM : M ⊆ 𝔅.members) : (𝔅.restrict M hM).members = M

theorem Utilities.Treewidth.Bramble.exists_inter_or_adj {V : Type u} [DecidableEq V] {H : SimpleGraph V} (𝔅 : Bramble H) {B B' : Finset V} (hB : B ∈ 𝔅.members) (hB' : B' ∈ 𝔅.members) : (B ∩ B').Nonempty ∨ ∃ x ∈ B, ∃ y ∈ B', H.Adj x y

Two members of a bramble either share a vertex or are joined by an edge.

This is the combinatorial content of touching and is what TreewidthGonality/Gonality/BrambleGonality.lean consumes when it builds a hitting set out of a cut.

Proved (2026-08-25): touching B hB B' hB' gives a walk inside ↑(B ∪ B') from a vertex of B to a vertex of B' (both are nonempty). If B ∩ B' = ∅ the endpoint of that walk is outside the subtype-level set {x | ↑x ∈ B}, so exists_adj_across_of_walk produces an edge of the induced graph with one end in B and the other in (B ∪ B') ∖ B = B' ∖ B; SimpleGraph.comap_adj pushes it back down to an edge of H.

theorem Utilities.Treewidth.Bramble.isHittingSet_univ {V : Type u} [DecidableEq V] {H : SimpleGraph V} (𝔅 : Bramble H) [Fintype V] : 𝔅.IsHittingSet Finset.univ

All of V is a hitting set, because members are nonempty.

theorem Utilities.Treewidth.Bramble.hittingSetCards_nonempty {V : Type u} [DecidableEq V] {H : SimpleGraph V} (𝔅 : Bramble H) [Finite V] : 𝔅.hittingSetCards.Nonempty

Hitting sets exist, so order is an infimum over a nonempty set.

theorem Utilities.Treewidth.Bramble.exists_isHittingSet_card_eq_order {V : Type u} [DecidableEq V] {H : SimpleGraph V} (𝔅 : Bramble H) [Finite V] : ∃ (S : Finset V), 𝔅.IsHittingSet S ∧ S.card = 𝔅.order

The order is realized by an actual hitting set.

theorem Utilities.Treewidth.Bramble.order_le_card {V : Type u} [DecidableEq V] {H : SimpleGraph V} (𝔅 : Bramble H) [Fintype V] : 𝔅.order ≤ Fintype.card V

order 𝔅 ≤ |V|.

theorem Utilities.Treewidth.Bramble.exists_disjoint_of_card_lt_order {V : Type u} [DecidableEq V] {H : SimpleGraph V} (𝔅 : Bramble H) {S : Finset V} (hS : S.card < 𝔅.order) : ∃ B ∈ 𝔅.members, B ∩ S = ∅

The form the main proof uses: a set too small to be a hitting set misses some member outright.

theorem Utilities.Treewidth.Bramble.one_le_order {V : Type u} [DecidableEq V] {H : SimpleGraph V} (𝔅 : Bramble H) [Finite V] (h : 𝔅.members.Nonempty) : 1 ≤ 𝔅.order

A bramble with at least one member has positive order.

theorem Utilities.Treewidth.Bramble.order_restrict_le {V : Type u} [DecidableEq V] {H : SimpleGraph V} (𝔅 : Bramble H) [Finite V] (M : Finset (Finset V)) (hM : M ⊆ 𝔅.members) : (𝔅.restrict M hM).order ≤ 𝔅.order

Monotonicity of the order under passing to a subfamily: fewer members are easier to hit.