Catalog.Sparsity.ColoringNumbers

Definition

Let \(G\) be a graph, let \(\sigma\) be a vertex ordering of \(G\), and let \(r \in \mathbb{N}\). For vertices \(u, v \in V(G)\) with \(u \leq_\sigma v\):

\(u\) is strongly \(r\)-reachable from \(v\) if there is a path of length at most \(r\) from \(u\) to \(v\) whose every internal vertex \(w\) satisfies \(v <_\sigma w\).
\(u\) is weakly \(r\)-reachable from \(v\) if there is a path of length at most \(r\) from \(u\) to \(v\) whose every internal vertex \(w\) satisfies \(u <_\sigma w\).

The sets of vertices strongly (resp. weakly) \(r\)-reachable from \(v\) are denoted \(\operatorname{SReach}_r[G, \sigma, v]\) (resp. \(\operatorname{WReach}_r[G, \sigma, v]\)).

The weak and strong \(r\)-coloring numbers of \(\sigma\) are then \[\begin{aligned} \operatorname{wcol}_r(G, \sigma) &\coloneqq \max_{v \in V(G)} |\operatorname{WReach}_r[G, \sigma, v]|, \\ \operatorname{scol}_r(G, \sigma) &\coloneqq \max_{v \in V(G)} |\operatorname{SReach}_r[G, \sigma, v]|. \end{aligned}\]

Review notes

This entry merges the reachability definitions (Def 2.1) with the wcol/scol parts of Def 2.3. The adm part of Def 2.3 is formalized separately in Definition Admissibility together with per-vertex admissibility (Def 2.2); both entries’ source.tex therefore reproduce Def 2.3 in full, but 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. A consequence is that the graph-level minimums \(\operatorname{wcol}_r(G)\), \(\operatorname{scol}_r(G)\), \(\operatorname{adm}_r(G)\) over all orderings are not formalized here; they would require quantifying over all linear orders on the vertex type.

SReach and WReach are defined as Set V. Membership requires \(u \leq v\), a path witness of length \(\leq r\), and the appropriate constraint on internal vertices (all \(> v\) for strong, all \(> u\) for weak). The source uses “path” throughout; Lean models these as SimpleGraph.Walk values satisfying IsPath.

Cardinalities of SReach and WReach use Set.ncard (natural-number-valued cardinality for sets).

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

1	import Mathlib.Combinatorics.SimpleGraph.Walk.Basic
2	import Mathlib.Combinatorics.SimpleGraph.Paths
3	import Mathlib.Data.Set.Card
4
5	namespace Catalog.Sparsity.ColoringNumbers
6
7	variable {V : Type*} [DecidableEq V] [Fintype V] [LinearOrder V]
8
9	/-- The set of vertices strongly r-reachable from `v` with respect to the
10	linear order on `V`. A vertex `u ≤ v` is in `SReach G r v` when there
11	exists a path of length ≤ r from `v` to `u` whose internal vertices
12	are all strictly greater than `v`. (Def 2.1) -/
13	def SReach (G : SimpleGraph V) (r : ℕ) (v : V) : Set V :=
14	{u \| u ≤ v ∧ ∃ p : G.Walk v u, p.IsPath ∧ p.length ≤ r ∧
15	∀ i : ℕ, 0 < i → i < p.length → v < p.getVert i}
16
17	/-- The set of vertices weakly r-reachable from `v` with respect to the
18	linear order on `V`. A vertex `u ≤ v` is in `WReach G r v` when there
19	exists a path of length ≤ r from `v` to `u` whose internal vertices
20	are all strictly greater than `u`. (Def 2.1) -/
21	def WReach (G : SimpleGraph V) (r : ℕ) (v : V) : Set V :=
22	{u \| u ≤ v ∧ ∃ p : G.Walk v u, p.IsPath ∧ p.length ≤ r ∧
23	∀ i : ℕ, 0 < i → i < p.length → u < p.getVert i}
24
25	open Classical in
26	/-- The weak r-coloring number of `G` (per ordering): the maximum over
27	all vertices of the cardinality of the weak r-reachability set. (Def 2.3) -/
28	noncomputable def wcol (G : SimpleGraph V) (r : ℕ) : ℕ :=
29	Finset.sup Finset.univ (fun v => (WReach G r v).ncard)
30
31	open Classical in
32	/-- The strong r-coloring number of `G` (per ordering): the maximum over
33	all vertices of the cardinality of the strong r-reachability set. (Def 2.3) -/
34	noncomputable def scol (G : SimpleGraph V) (r : ℕ) : ℕ :=
35	Finset.sup Finset.univ (fun v => (SReach G r v).ncard)
36
37	end Catalog.Sparsity.ColoringNumbers
38

Used By

Statement