Lax12.AdmissibilityBound

Admissibility is bounded by topological shallow-minor density

concepts/Lax12/AdmissibilityBound.lean · lax-12

proven

Loading review…

Concept map

Proven claimDefinitionThis conceptRelated conceptA → B: B builds on A

Evidence

Each proof establishes this claim relative to its assumptions.

no assumptions

thm✓Lax12.AdmissibilityBound

⊢Lax12Proofs.AdmissibilityBound.adm_le_of_hasTopologicalDensityAtMost

Theorem

If every depth-r topological minor of a graph G has at most d · |V| edges, then the (r+1)-admissibility of G is at most 1 + 6 · (r+1) · d³. This is the workhorse behind every bound of a generalized coloring number by an edge-density bound: sparse shallow topological minors force an ordering in which no vertex reaches many predecessors along disjoint short paths.

The source lecture notes state this as Lemma 3.2 of Chapter 2 (2019/20 edition): for every r and every graph G, $\operatorname{adm}_r(G) \le 1 + 6r\lceil\tilde\nabla_{r-1}(G)\rceil^3$ , where $\tilde\nabla$ is the topological grad.

Lean source view on GitHub

1	import Lax12.Admissibility
2	import Lax12.ShallowTopologicalMinors
3
4	/-!
5	---
6	title: Admissibility is bounded by topological shallow-minor density
7	type: theorem
8	---
9	If every depth-r topological minor of a graph G has at most
10	d · \|V\| edges, then the (r+1)-admissibility of G is at most
11	1 + 6 · (r+1) · d³. This is the workhorse behind every bound of a
12	generalized coloring number by an edge-density bound: sparse shallow
13	topological minors force an ordering in which no vertex reaches many
14	predecessors along disjoint short paths.
15
16	The source lecture notes state this as Lemma 3.2 of Chapter 2 (2019/20
17	edition): for every r and every graph G,
18	$\operatorname{adm}_r(G) \le 1 + 6r\lceil\tilde\nabla_{r-1}(G)\rceil^3$ , where
19	$\tilde\nabla$ is the topological grad.
20
21	# Formalization notes
22
23	Hypothesis and conclusion are the predicates of the two imported
24	definition concepts. The statement is the notes' Lemma 3.2 with its
25	radius index shifted by one: the notes pair a conclusion at radius r
26	with a hypothesis at depth r−1, and writing the conclusion at r+1
27	against a hypothesis at depth r keeps truncated natural subtraction
28	out of a concept statement. This is presentation only — the shifted form
29	ranges over exactly the instances r ≥ 1 of the notes' form, which are
30	all of its instances with a defined hypothesis, and the constant is the
31	notes' constant with r read as r+1.
32
33	The natural number d plays the notes' $\lceil\tilde\nabla_{r-1}(G)\rceil$ : the
34	hypothesis `HasTopologicalDensityAtMost G r d` says exactly that the
35	topological grad of G at depth r is at most d, and the notes
36	instantiate their lemma at the ceiling of that grad, the least natural
37	number with this property. The leading 1 of the bound is the vertex v
38	itself, which admissibility counts.
39	-/
40
41	namespace Lax12.AdmissibilityBound
42
43	open Lax12.Admissibility Lax12.ShallowTopologicalMinors
44
45	/-- A depth-`r` topological edge-density bound `d` for `G` bounds the
46	`(r+1)`-admissibility of `G` by `1 + 6 · (r+1) · d ^ 3`. -/
47	axiom adm_le_of_hasTopologicalDensityAtMost {n : ℕ} (G : SimpleGraph (Fin n))
48	(r d : ℕ) (h : HasTopologicalDensityAtMost G r d) :
49	adm G (r + 1) ≤ 1 + 6 * (r + 1) * d ^ 3
50
51	end Lax12.AdmissibilityBound
52

Show Proof

Formalization notes

Hypothesis and conclusion are the predicates of the two imported definition concepts. The statement is the notes' Lemma 3.2 with its radius index shifted by one: the notes pair a conclusion at radius r with a hypothesis at depth r−1, and writing the conclusion at r+1 against a hypothesis at depth r keeps truncated natural subtraction out of a concept statement. This is presentation only — the shifted form ranges over exactly the instances r ≥ 1 of the notes' form, which are all of its instances with a defined hypothesis, and the constant is the notes' constant with r read as r+1.

The natural number d plays the notes' $\lceil\tilde\nabla_{r-1}(G)\rceil$ : the hypothesis $HasTopologicalDensityAtMost G r d$ says exactly that the topological grad of G at depth r is at most d, and the notes instantiate their lemma at the ceiling of that grad, the least natural number with this property. The leading 1 of the bound is the vertex v itself, which admissibility counts.

Builds on

Used by

none

From Mathlib

none

Community review

Discussion

Ask a question or add context. Endorsements and structured flags are kept in the review panel above; your ORCID profile must share a public name.

0 comments

Loading discussion…

Lax Lean Archive