Catalog.Sparsity.ShallowMinor

Definition

A graph \(H\) is a minor of \(G\), written \(H \preccurlyeq G\), if there is a minor model \(\varphi\) of \(H\) in \(G\): a map \(\varphi\) which assigns to every vertex \(v \in V(H)\) a connected subgraph \(\varphi(v) \subseteq G\) and to every edge \(e \in E(H)\) an edge \(\varphi(e) \in E(G)\) such that:

if \(u, v \in V(H)\) with \(u \neq v\) then \(V(\varphi(v)) \cap V(\varphi(u)) = \emptyset\), and
if \(e = uv \in E(H)\) then \(\varphi(e) = u'v' \in E(G)\) for vertices \(u' \in V(\varphi(u))\) and \(v' \in V(\varphi(v))\).

The set \(\varphi(v)\) is the branch set of \(v\).

The radius of a connected graph \(G\) is \(\operatorname{rad}(G) = \min_{u \in V(G)} \max_{v \in V(G)} \operatorname{dist}(u, v)\).

Let \(H\), \(G\) be graphs and let \(d \in \mathbb{N}\). The graph \(H\) is a depth-\(d\) minor of \(G\), written \(H \preccurlyeq_d G\), if there is a minor model \(\varphi\) of \(H\) in \(G\) such that the branch set \(\varphi(v)\) has radius at most \(d\) for all \(v \in V(H)\).

For a graph \(G\) and \(d \in \mathbb{N}\): \[\nabla_d(G) := \sup \left\{ \frac{|E(H)|}{|V(H)|} : H \preccurlyeq_d G \right\}, \qquad \omega_d(G) := \sup \left\{ t : K_t \preccurlyeq_d G \right\}.\] For a graph class \(\mathcal{C}\) and \(d \in \mathbb{N}\): \[\nabla_d(\mathcal{C}) := \sup_{G \in \mathcal{C}} \nabla_d(G), \qquad \omega_d(\mathcal{C}) := \sup_{G \in \mathcal{C}} \omega_d(G).\]

Review notes

The Lean contract encodes depth-\(d\) minors as a structure type faithful to the source definition.

ShallowMinorModel. The structure carries a branch-set map, a center for each branch set, and proofs of the three properties: branch-set disjointness, bounded-radius connectivity within each branch set, and edge witnessing. The radius condition uses walks (not graph distance) to avoid dependence on metric infrastructure. Branch-set membership of every walk vertex is required explicitly, ensuring the walk stays inside the branch set. This matches Definition 2.3 of the source.

A full (unbounded) minor model corresponds to depth \(d = \infty\); in our formalization, omitting the depth bound is achieved by choosing \(d\) large enough (e.g., \(|V(G)|\)). We do not define an unbounded minor type separately, since the downstream theorems only use depth-bounded minors.

Omissions. The source also defines \(\nabla_d(G)\) and \(\omega_d(G)\) as numeric suprema. These are not formalized here because the downstream definitions (nowhere dense, bounded expansion) only need the predicate “\(K_t\) is not a depth-\(d\) minor,” which is directly expressed as \(\lnot\)IsShallowMinor. This avoids the need for rational- or real-valued supremum infrastructure.

Catalog/Sparsity/ShallowMinor/Contract.lean (full)

1	import Mathlib.Combinatorics.SimpleGraph.Walk.Basic
2	import Mathlib.Combinatorics.SimpleGraph.Paths
3
4	namespace Catalog.Sparsity.ShallowMinor
5
6	/-- A depth-`d` minor model of `H` in `G`.
7
8	For each vertex of `H` we choose a branch set in `G` together with a fixed
9	center. Every vertex of the branch set is connected to the center by a path of
10	length at most `d` that stays inside the branch set; distinct branch sets are
11	disjoint; and every edge of `H` is witnessed by an edge of `G` between the
12	corresponding branch sets. (Defs 1.10, 2.2-2.4) -/
13	structure ShallowMinorModel {V W : Type} (H : SimpleGraph W) (G : SimpleGraph V)
14	(d : ℕ) where
15	branchSet : W → Set V
16	center : W → V
17	center_mem : ∀ v, center v ∈ branchSet v
18	branchDisjoint : ∀ u v, u ≠ v → Disjoint (branchSet u) (branchSet v)
19	branchRadius : ∀ v x, x ∈ branchSet v →
20	∃ p : G.Walk (center v) x, p.IsPath ∧ p.length ≤ d ∧
21	∀ w ∈ p.support, w ∈ branchSet v
22	branchEdge : ∀ u v, H.Adj u v →
23	∃ x ∈ branchSet u, ∃ y ∈ branchSet v, G.Adj x y
24
25	/-- `H` is a depth-`d` minor of `G`. -/
26	def IsShallowMinor {V W : Type} (H : SimpleGraph W) (G : SimpleGraph V)
27	(d : ℕ) : Prop :=
28	Nonempty (ShallowMinorModel H G d)
29
30	end Catalog.Sparsity.ShallowMinor
31

Used By

Statement

Proof