Catalog.Sparsity.Admissibility

Definition

Let \(G\) be a graph, let \(\sigma\) be a vertex ordering of \(G\), and let \(r \in \mathbb{N}\). The \(r\)-admissibility of a vertex \(v\) of \(G\), denoted \(\operatorname{adm}_r(G, \sigma, v)\), is equal to one plus the maximum size of a family of paths \(\mathcal{P}\) with the following properties:

every path from \(\mathcal{P}\) has length at most \(r\) and leads from \(v\) to some vertex smaller than \(v\) in \(\sigma\);
paths from \(\mathcal{P}\) are pairwise vertex-disjoint apart from sharing the endpoint \(v\).

The \(r\)-admissibility of \(\sigma\) is \[\operatorname{adm}_r(G, \sigma) \coloneqq \max_{v \in V(G)} \operatorname{adm}_r(G, \sigma, v).\]

Review notes

This entry covers both per-vertex admissibility (Def 2.2) and the per-ordering admissibility adm from Def 2.3. The matching wcol/scol rows of Def 2.3 live in Definition ColoringNumbers, which also carries the reachability definitions (Def 2.1). Both entries’ source.tex reproduce Def 2.3 in full; each entry’s statement.tex covers only the rows it formalizes.

The vertex ordering \(\sigma\) is not passed explicitly. Instead, the vertex type carries an ambient LinearOrder V, so “smaller in \(\sigma\)” becomes \(<\) on V. The graph-level minimum \(\operatorname{adm}_r(G)\) over all orderings is not formalized here.

An admissible family is modeled as a structure IsAdmFamily whose fields encode the four conditions: targets strictly below \(v\), each member is a path (not just a walk), length at most \(r\), and pairwise vertex-disjointness except at the shared startpoint \(v\).

The per-vertex admissibility admVertex adds \(1\) to the supremum over family sizes, matching the source convention. The per-ordering adm is the Finset.sup of admVertex over all vertices.

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

1	import Mathlib.Combinatorics.SimpleGraph.Walk.Basic
2	import Mathlib.Combinatorics.SimpleGraph.Paths
3
4	open Classical
5
6	namespace Catalog.Sparsity.Admissibility
7
8	noncomputable section
9
10	variable {V : Type*} [DecidableEq V] [Fintype V] [LinearOrder V]
11
12	/-- An admissible family of paths at vertex `v`: an indexed collection of
13	paths from `v` to distinct vertices below `v` in the ordering, each of
14	length at most `r`, pairwise vertex-disjoint except at their shared
15	starting point `v`. (Def 2.2) -/
16	structure IsAdmFamily (G : SimpleGraph V) (r : ℕ) (v : V)
17	{ι : Type*} (paths : ι → (u : V) × G.Walk v u) : Prop where
18	target_lt : ∀ i, (paths i).1 < v
19	isPath : ∀ i, (paths i).2.IsPath
20	length_le : ∀ i, (paths i).2.length ≤ r
21	disjoint : ∀ i j, i ≠ j →
22	∀ w, w ∈ (paths i).2.support → w ∈ (paths j).2.support → w = v
23
24	/-- The r-admissibility of a vertex `v`: one plus the maximum size of an
25	admissible family of paths at `v`. (Def 2.2) -/
26	def admVertex (G : SimpleGraph V) (r : ℕ) (v : V) : ℕ :=
27	1 + Finset.sup (Finset.range (Fintype.card V)) (fun k =>
28	if ∃ (paths : Fin k → (u : V) × G.Walk v u), IsAdmFamily G r v paths
29	then k else 0)
30
31	/-- The r-admissibility of `G` (per ordering): the maximum over all vertices
32	of per-vertex r-admissibility. (Def 2.3) -/
33	def adm (G : SimpleGraph V) (r : ℕ) : ℕ :=
34	Finset.sup Finset.univ (fun v => admVertex G r v)
35
36	end
37
38	end Catalog.Sparsity.Admissibility
39

Used By

Statement

Proof

Catalog.Sparsity.NDSubpolynomialWcol