Quantitative bounds for Mazur’s greedy graph-drawing construction

For well-formed Mazur edge, cycle, series and join drawing schemes, determine the maximum span T in terms of vertex count n and nontrivial join count j. The sharp target is T+1≤2^j(n−2j), together with equality conditions and determinant or coordinate-height bounds.

Why it matters and what counts as progress

Why it matters: It quantifies geometric growth in a fixed drawing construction and the resulting algebraic quantities used for coordinates.

What counts as progress: Sharp span bounds for all permitted drawing schemes, attaining constructions, and controlled determinant or coordinate-height consequences.

How the problem developed

9 Sept 2026 · Construction [1][2]
Lech Mazur, with OpenAI Codex and GPT-6 Pro Released a proof candidate that every finite simple 3-connected plane graph has a convex greedy straight-line drawing, built using integer heights and a Dirichlet problem.
14 Sept 2026 · Quantitative analysis [2]
JD Jones Formalized bounds for Mazur's height-scheme recurrence and derived dart-weight and determinant bounds. The results do not bound the full drawing's area polynomially.

AI contribution

AI-derived bounds for Mazur’s greedy drawing construction

For a well-formed Mazur edge, cycle, series and join scheme with n≥2 vertices and j nontrivial joins, the span satisfies T+1≤2^j(n−2j), with equality at (n,j)=(2,0) or 2j+3≤n. Its worst case is T=2^(n/2)−1 for even n and T=3·2^((n−3)/2)−1 for odd n. Companion theorems give interior dart mass ≤aₛbₛT, Dirichlet row norm ≤2(n−1)²T and |det M|≤(2(n−1)²T)^n, bound the candidate products T²|det M| and T³|det M|, and prove z=adj(M)u with Mz=Δu and boundary zₛ=Δhₛ(T−hₛ) when hₛ≤T, where Δ=det M.

AI involvementAI-led

ImportanceModest

Technical verificationFormal (Lean 4/Mathlib kernel, Comparator and NanoDa)

Human understandingFew