Lax195003.WelzlOrdersComputation

Near-linear-time computation of Welzl orders

concepts/Lax195003/WelzlOrdersComputation.lean · lax-195003

open

Loading review…

Concept map

Open claimDefinitionThis conceptRelated conceptA → B: B builds on A

Evidence

Each proof establishes this claim relative to its assumptions.

No proof in the archive yet — this claim is open.

Theorem

Let C be a graph class whose members have neighborhood complexity at most c · k, for one constant c ≥ 1 shared by the class. There is a randomized algorithm which, given an n-vertex graph G in C and c, runs in $O((n+m) log n)$ time and, with probability at least 2/3, returns a total order of the vertices with crossing number at most 12c² log² n.

This is Theorem 1.3 of Dreier and Kuske, Near-Linear Time Computation of Welzl Orders on Graphs with Linear Neighborhood Complexity (2026).

Lean source view on GitHub

1	import Lax195003.WordRamRandomness
2	import Lax195003.WelzlOrdersInGraphs
3	import Lax195003.WelzlOrdersNeighborhoodComplexity
4	import Lax11.GraphEncoding
5	import Mathlib.Data.Nat.Log
6
7	/-!
8	---
9	title: Near-linear-time computation of Welzl orders
10	type: theorem
11	---
12	Let C be a graph class whose members have neighborhood complexity at most
13	c · k, for one constant c ≥ 1 shared by the class. There is a randomized
14	algorithm which, given an n-vertex graph G in C and c, runs in
15	`O((n+m) log n)` time and, with probability at least 2/3, returns a total order
16	of the vertices with crossing number at most 12c² log² n.
17
18	This is Theorem 1.3 of Dreier and Kuske, *Near-Linear Time Computation of
19	Welzl Orders on Graphs with Linear Neighborhood Complexity* (2026).
20
21	# Formalization notes
22
23	Linear neighborhood complexity is the separate definition
24	`Lax195003.WelzlOrdersNeighborhoodComplexity.HasLinearNeighborhoodComplexity`
25	in this submission, together with the per-graph predicate used below. They
26	define the neighborhood trace count and the graph's shatter function directly,
27	and require the genuinely linear bound `π_G(k) ≤ c · k`. The graph is
28	presented by the compressed sparse row encoding of Lax11, and the program runs
29	on the registered word RAM of Lax67 through this submission's finite-randomness
30	predicate.
31
32	The program and the constant `K` precede the graph class, its shared linearity
33	constant, the concrete member, the input word and the word length, so one
34	uniform program realizes the whole algorithm. Membership `C n G` explicitly
35	restricts the encoded inputs to graphs in the class. Its input is `c :: x`
36	followed by the random tape. The time bound
37	`K · (\|x\|+1) · (⌈log₂ n⌉+1)` is an elementary form of
38	`O((n+m) log n)`: a compressed sparse row word has length `3+n+2m`, up to
39	any repetitions present in the representation. The added ones make the bound
40	meaningful for the empty and one-vertex graphs and change it only by a
41	constant factor.
42
43	The paper writes a real-valued base-two logarithm. Its use in the natural
44	crossing and time bounds is read as `Nat.clog 2 n`, the ceiling binary
45	logarithm; this rounds the displayed upper bound upward rather than silently
46	strengthening it at non-powers of two.
47
48	The word-length condition says that the input, every value in it, and a
49	linear amount of working memory fit into a word-addressed machine. It follows
50	the convention of Lax11's algorithmic statements and is separate from the
51	running-time bound. The random tape has the same length as the time bound;
52	unused trailing bits do not affect its uniform success probability.
53
54	The output is relational rather than a preselected function of the graph:
55	any encoded vertex order meeting the paper's explicit crossing bound for the
56	open radius-one neighborhood system is a successful output. Radius one is the
57	ordinary open-neighborhood specialization of the general `k`-neighborhood
58	Welzl-order definition in `Lax195003.WelzlOrdersInGraphs`. Thus the statement
59	preserves the mathematical content of a randomized search algorithm without
60	imposing an arbitrary tie-breaking rule absent from the paper.
61	-/
62
63	namespace Lax195003.WelzlOrdersComputation
64
65	open Lax11.GraphEncoding
66	open Lax12.GraphClasses
67	open Lax67.Ram
68	open Lax195003.WelzlOrdersNeighborhoodComplexity
69	open Lax195003.WordRamRandomness Lax195003.WelzlOrdersInGraphs
70
71	/-- Near-linear computation of graph Welzl orders (Dreier–Kuske,
72	Theorem 1.3): one randomized word-RAM program, given a member of a graph class
73	whose neighborhood complexity is uniformly at most `c · k`, returns with
74	probability at least `2/3` an order with crossing number at most
75	`12 · c^2 · log₂(n)^2`, within a constant multiple of `(n+m) log n` steps. -/
76	axiom exists_nearLinearTime_randomized_welzlOrder_program :
77	∃ (p : Program) (K : ℕ), 1 ≤ K ∧
78	∀ (C : GraphClass) (c : ℕ), 1 ≤ c →
79	(∀ (n : ℕ) (G : SimpleGraph (Fin n)), C n G →
80	HasLinearNeighborhoodComplexityWithConstant G c) →
81	∀ (n : ℕ) (G : SimpleGraph (Fin n)), C n G →
82	∀ (w : ℕ) (x : List ℕ), EncodesGraph x n G →
83	(∀ v ∈ c :: x, K * (x.length + v + 1) ≤ 2 ^ w) →
84	let T := K * (x.length + 1) * (Nat.clog 2 n + 1)
85	SucceedsWithProbabilityAtLeastInTime
86	(2 / 3 : ℚ) w p (c :: x) T T
87	(EncodesGraphWelzlOrder G
88	1
89	(12 * c ^ 2 * (Nat.clog 2 n) ^ 2))
90
91	end Lax195003.WelzlOrdersComputation
92

Formalization notes

Linear neighborhood complexity is the separate definition $Lax195003.WelzlOrdersNeighborhoodComplexity.HasLinearNeighborhoodComplexity$ in this submission, together with the per-graph predicate used below. They define the neighborhood trace count and the graph's shatter function directly, and require the genuinely linear bound $π_G(k) ≤ c · k$ . The graph is presented by the compressed sparse row encoding of Lax11, and the program runs on the registered word RAM of Lax67 through this submission's finite-randomness predicate.

The program and the constant $K$ precede the graph class, its shared linearity constant, the concrete member, the input word and the word length, so one uniform program realizes the whole algorithm. Membership $C n G$ explicitly restricts the encoded inputs to graphs in the class. Its input is $c :: x$ followed by the random tape. The time bound $K · (|x|+1) · (⌈log₂ n⌉+1)$ is an elementary form of $O((n+m) log n)$ : a compressed sparse row word has length $3+n+2m$ , up to any repetitions present in the representation. The added ones make the bound meaningful for the empty and one-vertex graphs and change it only by a constant factor.

The paper writes a real-valued base-two logarithm. Its use in the natural crossing and time bounds is read as $Nat.clog 2 n$ , the ceiling binary logarithm; this rounds the displayed upper bound upward rather than silently strengthening it at non-powers of two.

The word-length condition says that the input, every value in it, and a linear amount of working memory fit into a word-addressed machine. It follows the convention of Lax11's algorithmic statements and is separate from the running-time bound. The random tape has the same length as the time bound; unused trailing bits do not affect its uniform success probability.

The output is relational rather than a preselected function of the graph: any encoded vertex order meeting the paper's explicit crossing bound for the open radius-one neighborhood system is a successful output. Radius one is the ordinary open-neighborhood specialization of the general $k$ -neighborhood Welzl-order definition in $Lax195003.WelzlOrdersInGraphs$ . Thus the statement preserves the mathematical content of a randomized search algorithm without imposing an arbitrary tie-breaking rule absent from the paper.

Builds on

Used by

none

From Mathlib

Mathlib.Data.Nat.Log

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