Construction sequences with few realized types

Lax185574.FewTypes · concepts/Lax185574/FewTypes.lean · lax-185574

proven

Loading review…

Natural Language Statement

Theorem

Let 𝒞 be a monadically dependent graph class, r, q ∈ ℕ, and let ε > 0 be a rational. There is a constant α ≥ 1 depending only on 𝒞 and q such that every graph G ∈ 𝒞 has a construction sequence of radius-r depth-q width O_{𝒞,r,q,ε}(n^{αε}) and length O_{𝒞,r,q,ε}(n^{1+αε}). Moreover, there is an algorithm (independent of 𝒞) which, given r, q ∈ ℕ, a rational ε > 0 and an n-vertex graph G ∈ 𝒞, computes such a construction sequence in time Ô_{𝒞,r,q,ε}(n³). Here Ô_k(n³) stands for a bound O_{k,η}(n^{3+η}) for every η > 0.

It is important that α does not depend on ε, as this makes the exponent αε of the width as small as one likes.

Concept map

14 concepts

100%

Proven claimDefinitionThis conceptRelated conceptA → B: B builds on A

Evidence

Each proof establishes this claim relative to its assumptions.

- thm✓Lax185574.DefinableSequences
- thm✓Lax185574.DefinableToTypes
→
thm✓Lax185574.FewTypes
⊢Lax185574Proofs.FewTypes.exists_program_fewTypes

In the paper

page 14 of this submission's paper

Lean source view on GitHub

Show types on hover

1	import Lax185574.Width
2	import Lax185574.ConstructionSequences
3	import Lax185574.MonadicDependence
4	import Lax185574.Algorithms
5	import Mathlib.Analysis.SpecialFunctions.Pow.Real
6
7	/-!
8	---
9	title: Construction sequences with few realized types
10	type: theorem
11	---
12	Let 𝒞 be a monadically dependent graph class, r, q ∈ ℕ, and let ε > 0
13	be a rational. There is a constant α ≥ 1 depending only on 𝒞 and q such
14	that every graph G ∈ 𝒞 has a construction sequence of radius-r depth-q
15	width O_{𝒞,r,q,ε}(n^{αε}) and length O_{𝒞,r,q,ε}(n^{1+αε}). Moreover,
16	there is an algorithm (independent of 𝒞) which, given r, q ∈ ℕ, a
17	rational ε > 0 and an n-vertex graph G ∈ 𝒞, computes such a
18	construction sequence in time Ô_{𝒞,r,q,ε}(n³). Here Ô_k(n³) stands for
19	a bound O_{k,η}(n^{3+η}) for every η > 0.
20
21	It is important that α does not depend on ε, as this makes the exponent
22	αε of the width as small as one likes.
23
24	# Formalization notes
25
26	The shape is that of `Lax185574.DefinableSequences`. The construction
27	sequence is produced by a function `script` of r, q, ε and the graph,
28	and the algorithm `A` computes this function. Neither depends on 𝒞. On
29	every graph, the script gives a construction sequence of the graph, and
30	the numbers in its encoding are small (`Script.HasSmallNumbers`). The
31	input of the algorithm is the quadruple (r, q, ε, G). The constant α of
32	the paper is `a`. It is chosen after the class and q, and before r and
33	ε. The width is the radius-r depth-q width of `Lax185574.Width`.
34
35	Every number in the encoding of the script is at most the length of the
36	encoding plus n. The paper does not say this. The algorithm can ensure
37	it by giving the vertices of the initial partial graph the colors
38	0, …, n − 1, since steps only use colors that occur.
39
40	The time bound Ô_{𝒞,r,q,ε}(n³) is spelled out as `n^(3+η)` for every
41	real η > 0, with the constant `c` depending on 𝒞, r, q, ε and η. The
42	same `c` bounds the sequence.
43	-/
44
45	namespace Lax185574.FewTypes
46
47	open Lax185574.Graphs Lax185574.MonadicDependence Lax185574.Algorithms
48	open Lax185574.ConstructionSequences Lax185574.Width
49
50	/-- Construction sequences with few realized types. One algorithm
51	computes, from `r`, `q`, a rational `ε > 0` and a graph `G`, a
52	construction sequence of `G`, given by its script. On members of a
53	monadically dependent class it takes time `O(n^(3+η))` for every
54	`η > 0`, and the sequence has length at most `c · (n+1)^(1+aε)` and
55	radius-`r` depth-`q` width at most `c · (n+1)^(aε)`. Here `a ≥ 1`
56	depends only on the class and `q`, and `c` on the class, `r`, `q`, `ε`
57	and `η`. -/
58	axiom exists_program_fewTypes :
59	∃ (A : Algorithm) (script : ℕ → ℕ → ℚ → (G : Graph) → Script G.n),
60	(∀ (r q : ℕ) (ε : ℚ) (G : Graph), 0 < ε →
61	IsConstructionSequence G.toSimpleGraph (script r q ε G).run ∧
62	(script r q ε G).HasSmallNumbers) ∧
63	∀ C : GraphClass, MonadicallyDependent C → ∀ q : ℕ, ∃ a : ℕ, 1 ≤ a ∧
64	∀ (r : ℕ) (ε : ℚ), 0 < ε → ∀ η : ℝ, 0 < η → ∃ c : ℕ,
65	∀ G ∈ C,
66	A.Computes c (r, q, ε, G) (script r q ε G) ((G.n : ℝ) ^ (3 + η)) ∧
67	((script r q ε G).run.length : ℝ) ≤ c * ((G.n : ℝ) + 1) ^ (1 + (a : ℝ) * ε) ∧
68	(width r q (script r q ε G).run : ℝ) ≤ c * ((G.n : ℝ) + 1) ^ ((a : ℝ) * ε)
69
70	end Lax185574.FewTypes
71

Show Proof

Formalization notes

The shape is that of $Lax185574.DefinableSequences$ . The construction sequence is produced by a function $script$ of r, q, ε and the graph, and the algorithm $A$ computes this function. Neither depends on 𝒞. On every graph, the script gives a construction sequence of the graph, and the numbers in its encoding are small ( $Script.HasSmallNumbers$ ). The input of the algorithm is the quadruple (r, q, ε, G). The constant α of the paper is $a$ . It is chosen after the class and q, and before r and ε. The width is the radius-r depth-q width of $Lax185574.Width$ .

Every number in the encoding of the script is at most the length of the encoding plus n. The paper does not say this. The algorithm can ensure it by giving the vertices of the initial partial graph the colors 0, …, n − 1, since steps only use colors that occur.

The time bound Ô_{𝒞,r,q,ε}(n³) is spelled out as $n^(3+η)$ for every real η > 0, with the constant $c$ depending on 𝒞, r, q, ε and η. The same $c$ bounds the sequence.

Builds on

Used by

none

From Mathlib

Mathlib.Analysis.SpecialFunctions.Pow.Real

Discussion

Ask a question or add context. Endorsements and structured flags are kept in the review panel above.

Loading discussion…

Lax Lean Archive

Construction sequences with few realized types

Flags

Flag this concept

Natural Language Statement

Theorem

In the paper

Lean source view on GitHub

Discussion

Settings

Your comments