Completed

Periodic Multidimensional Costas Arrays (Rubio–Torres Conjecture 1)Open Problem

Motivation

A Costas array is a permutation matrix in which the difference vectors between distinct dots are pairwise distinct; such arrays are frequency-hopping patterns for sonar and radar (Costas, 1984). Rubio and Torres ask whether their $m$ -dimensional version can stay Costas in every window of its periodic extension, and conjecture that this happens only in the smallest order.

Timeline. 1984: Taylor proves that 2D periodic Costas arrays have order $\le 2$ . 2023: Rubio–Torres prove the odd-order and 3D cases, give $2\times2\times4$ examples, and state Conjecture 1.

Setting

Let $[n]=\{1,\dots,n\}$ , $X=[a_1]\times\cdots\times[a_k]$ , $Y=[b_1]\times\cdots\times[b_l]$ with all sides $\ge2$ , and $\varphi:X\to Y$ a bijection; the dots are $(x,\varphi(x))\in\mathbb Z^{k+l}$ . The array is Costas if the difference vectors between distinct dots are distinct, and periodic Costas if moreover, after repeating the dots periodically over $\mathbb Z^{k+l}$ , the dots inside every translate $t+X\times Y$ have distinct difference vectors.

Formalization target

Conjecture 1: if $k\ge l\ge1$ and $\varphi$ defines a periodic Costas array, then

\prod_{i=1}^k a_i=2^k,

equivalently every $a_i=2$ . The condition $k\ge l$ is a normalization ( $\varphi^{-1}$ swaps the boxes).

Significance

A proof would give the multidimensional analogue of Taylor's theorem; a counterexample would give periodic distinct-difference patterns of non-power-of-two order.

Difficulty

The Rubio–Torres counting argument needs a bound that is available only when $Y$ is one-dimensional, which is why it stops at $m=3$ . Computational evidence: an exhaustive window check reports that the $2\times3\times2\times3$ array with dots $(1,1,1,1),(1,2,1,2),(1,3,2,1),(2,1,1,3),(2,2,2,3),(2,3,2,2)$ is periodic Costas, which would disprove the conjecture.

Formalization scope

A point of $\mathbb Z^{k+l}$ is a pair $(x,y)$ ; boxes are 1-based; $\varphi$ is a total function $\mathbb Z^k\to\mathbb Z^l$ whose values off $X$ are unused. Differences are plain integer vectors (not reduced modulo the sides), windows range over all $t\in\mathbb Z^{k+l}$ , and $k,l\ge1$ and sides $\ge2$ are part of the definition, so no degenerate case holds vacuously.

Selected references

I. Rubio, J. Torres, Multidimensional Costas Arrays and Their Periodicity, IEEE Trans. Inf. Theory 69(8), 2023, 5032–5040. arXiv:2208.02378, DOI
J. P. Costas, A study of a class of detection waveforms having nearly ideal range-Doppler ambiguity properties, Proc. IEEE 72(8), 1984, 996–1009.
S. W. Golomb, H. Taylor, Constructions and properties of Costas arrays, Proc. IEEE 72(9), 1984, 1143–1163.

2 thms1 active userReviewed

Graph Theory Operations Research·Captain: mikedeng1

The Strong Perfect Graph Theorem I: A Graph Is Perfect If and Only If It Is BergeResearch Paper

Motivation

A perfect graph is one whose coloring problem has a particularly sharp answer on every induced subgraph: the fewest colors needed is exactly the size of its largest clique. This makes a local obstruction, a clique, certify the optimum number of colors throughout the graph. Claude Berge proposed in 1961 that perfection could be recognized by the absence of two kinds of induced odd cycles, one in the graph and one in its complement. The equivalence became known as the strong perfect graph conjecture. Chudnovsky, Robertson, Seymour, and Thomas proved it in their 2006 paper, which also proves a structural decomposition of the graphs under study. The paper connects this question to graph coloring, Shannon capacity, and linear and integer programming. Chudnovsky et al., pp. 51–54

The earlier complement theorem was proved by Lovász in 1972 and appears as Theorem 1.1 in the paper. The strong conjecture remained unresolved for roughly four decades; the authors' Theorem 1.2 settles it. Their proof places a second result, Theorem 1.3, beside the equivalence: a graph with no forbidden odd hole or antihole must either belong to a basic class or admit one of several specified decompositions. The graph classes and decompositions are therefore part of the statement of the route to the main result, not merely vocabulary for a proof. Chudnovsky et al., pp. 52–56

Setting

All graphs here are finite and simple. The complement $\overline G$ has the same vertices as $G$ , and two distinct vertices are adjacent in $\overline G$ exactly when they are not adjacent in $G$ . For a vertex set $X$ , the notation $G|X$ means the induced subgraph on $X$ . A clique is a set of pairwise adjacent vertices. Its largest possible size in a graph $H$ is $\omega(H)$ , and $\chi(H)$ is the minimum number of colors in a proper vertex coloring of $H$ .

A hole is an induced cycle of length at least four. An antihole of $G$ is a hole in $\overline G$ . A graph is Berge if every hole and antihole has even length. Thus a perfect graph requires $\chi(G|X)=\omega(G|X)$ for every $X\subseteq V(G)$ , while a Berge graph satisfies a restriction on induced cycles in both $G$ and $\overline G$ . “Induced” matters: a cycle with a chord is not a hole. Chudnovsky et al., pp. 51–52

For the structural milestones, a basic graph is a bipartite graph, the complement of one, a line graph of a bipartite graph, the complement of such a line graph, or a double split graph. The latter consists of paired vertices $a_i,b_i$ and $c_j,d_j$ with the within-pair and between-pair adjacencies specified on pp. 52–53. A proper 2-join partitions the vertices into two sides with two prescribed complete cross-edge blocks, connected-component conditions on both sides, and a special odd-path condition. A proper homogeneous pair is a pair of vertex sets whose outside vertices split into four nonempty adjacency classes. A balanced skew partition has one side disconnected and the other disconnected in the complement, together with parity restrictions on induced paths and antipaths. Chudnovsky et al., pp. 52–54

Formalization targets

Theorem 1.2: perfection and the Berge property

The goal is the exact equivalence for every finite simple graph:

G\text{ is perfect}\quad\Longleftrightarrow\quad G\text{ is Berge}.

No order bound, chosen graph class, or decomposition hypothesis is attached to the goal. Chudnovsky et al., p. 52, 1.2

Structural and reduction milestones

Theorem 1.1 says that $G$ perfect implies $\overline G$ perfect. Theorem 1.5 says that a minimum imperfect graph, a Berge nonperfect graph with the smallest vertex count among all such graphs, cannot admit a balanced skew partition. Theorem 13.5 says that a recalcitrant graph—a Berge graph with the listed line-graph, double-split, 2-join, homogeneous-pair, and balanced-skew outcomes absent—has $G$ or $\overline G$ bipartite. Theorem 1.3 states the decomposition conclusion:

G\text{ Berge}\Longrightarrow G\text{ basic}\ \lor\ G\text{ or }\overline G\text{ has a proper 2-join}\ \lor\ G\text{ has a proper homogeneous pair}\ \lor\ G\text{ has a balanced skew partition}.

The milestone order records the two reduction results, the later structural capstone, and the decomposition statement it yields. The paper's other section results that establish 13.5 are posed in the remaining missions of this series. Chudnovsky et al., pp. 52, 54–55, 154

Significance

Theorem 1.2 gives a forbidden-induced-subgraph characterization of perfect graphs. Its cycle condition is intrinsic to the graph and its complement; its coloring condition quantifies over every induced subgraph. Together with Theorem 1.3, it ties a numerical property of colorings to explicit graph structures and separations. The complement theorem and the exclusion of decompositions for a minimum imperfect graph explain why the structural alternatives have the strength needed for the equivalence. Chudnovsky et al., pp. 52–56

The mathematical theorem was proved in the cited paper. This mission poses its statements in Lean and seeks machine-checked proofs; the draft theorem declarations are open targets. The definition layer is useful beyond this mission: induced holes, Berge graphs, perfection, balanced skew partitions, and the decomposition predicates can support the later missions without changing what each source statement means. No machine-checked proof of these draft targets is claimed here.

Difficulty

The forward implication can be tested on induced odd cycles, but that observation does not settle the converse. Excluding odd holes and antiholes does not give an immediate coloring of an arbitrary induced subgraph. The paper instead establishes a detailed account of what a Berge graph can look like when it is not in a basic class. The delicate point in turning this account into Theorem 1.2 is that each decomposition outcome must be incompatible with a minimum imperfect graph. Ordinary skew partitions are too broad for that role; the balanced parity conditions are part of the statement. The structural conclusion 13.5 collects restrictions established across many later sections, so formalizing its prerequisites is a substantial graph-theoretic task. Chudnovsky et al., pp. 52–56, 154

Formalization scope

Lean uses SimpleGraph V with finite vertices, decidable vertex equality, and the Mathlib complement, induced subgraph, chromatic number, clique number, bipartiteness, and line graph. A hole is a list in cyclic order whose adjacency relation agrees exactly with the cycle edges; a path is likewise listed in one orientation with exactly its consecutive edges. Antiholes and antipaths use the complement graph. The empty vertex set is connected, matching p. 54. The double split partition is encoded by an equivalence from the four indexed parts to the whole vertex type, making disjointness and coverage explicit. A minimum imperfect graph is globally minimal by vertex count, among all finite Berge graphs.

No hypothesis beyond the paper's finite, simple graph convention is added to the goal or numbered milestones. In particular, “Berge” includes holes in both $G$ and $\overline G$ ; “perfect” ranges over every induced subgraph; and the complement occurs only in those decomposition outcomes where the paper places it. A non-induced cycle or a missing complement condition would make the formal target different. The definitions and Lean proofs of the graph classes, their boundary cases, and the structural milestones are welcome contributions. Later missions pose the paper's intervening numbered results rather than duplicating them here.

Selected references

Maria Chudnovsky, Neil Robertson, Paul Seymour, and Robin Thomas, The strong perfect graph theorem, Annals of Mathematics 164 (2006), 51–229. DOI 10.4007/annals.2006.164.51.

15 thms1 active userReviewed

Completed

Captain: mysticflounder

Six-colour Schur colourings of [1, 1801] under R₄(3) ≤ 61: balanced classes, nested saturation and forced reflectionResearch Paper

Motivation

The Schur number $S(n)$ is the largest $N$ such that $[1, N] = \{1, \dots, N\}$ can be partitioned into $n$ sumfree sets, sets with no $x, y, z$ such that $x + y = z$ ( $x = y$ allowed). Schur's argument gives $S(n) \le R_n(3) - 2$ , where the triangle Ramsey number $R_n(3)$ is the least $N$ such that every colouring of the edges of $K_N$ with $n$ colours has a monochromatic triangle (Fredricksen–Sweet 2000, inequality (2)). Only $S(1), \dots, S(5) = 1, 4, 13, 44, 160$ are known (Heule 2018). For six colours the published range is $536 \le S(6) \le 1836$ ; the upper bound is $R_6(3) - 2$ with $R_6(3) \le 1838$ (DS1, rev. 18).

Timeline.

1955: Greenwood and Gleason prove $R_3(3) = 17$ and $R_{n+1}(3) \le (n+1)(R_n(3) - 1) + 2$ (Theorem 6) (doi).
1961: Baumert finds $S(4) = 44$ by computer, as reported by Fredricksen and Sweet; they and Heule cite Golomb–Baumert 1965 for it.
1973: Chung proves $R_4(3) \ge 51$ (doi).
1997: Wan bounds $R_n(3)$ and, for even $n \ge 6$ , states $S_n < n!\,(e - e^{-1} + 3)/2 - n + 2$ (zbMATH 0882.05095 summary; doi). If his $S_n$ is the least $N$ that forces a monochromatic solution, this is the centred bound below, applied to his own bound on $R_{n-1}(3)$ ; if it is the largest $N$ , it is $1$ above it. His proof was not read.
2000: Fredricksen and Sweet prove $S(6) \ge 536$ (doi).
2004: Fettes, Kramer and Radziszowski prove $R_4(3) \le 62$ (listed in DS1, which also lists $R_5(3) \le 307$ ).
2018: Heule proves $S(5) = 160$ with a certified SAT computation (AAAI-18; preprint arXiv:1711.08076).
2026: a public repository of M. Tatarevic gives a computer-assisted argument for $R_4(3) \le 61$ . Its Lean development assumes that a family of 56,830 SAT instances is unsatisfiable, and the repository records solver results for them. The project of this mission's author produced LRAT certificates for all 56,830 instances and checked them; the report is in the repository's issue tracker. This mission does not depend on it.

The first target is a centred-interval bound: if $R_k(3) \le r$ , then $S(k+1) \le 2(k+1)\lfloor (r-1)/2 \rfloor + 1$ . With $R_4(3) \le 61$ the recursive bound gives $R_5(3) \le 302$ , and the centred bound gives $S(6) \le 1801$ ; with $R_5(3) \le 307$ it gives only $1837$ . The mission formalizes what a Schur colouring of $[1, 1801]$ with six colours would have to look like under $R_4(3) \le 61$ .

Setting

All numbers are natural numbers, $\mathbb{N} = \{0, 1, 2, \dots\}$ , and $[a, b] = \{a, \dots, b\}$ .

Schur colourings and covers. A colouring with $n$ colours is a map $c : \mathbb{N} \to \mathrm{Fin}\,n$ . It is a Schur colouring of $[1, N]$ (SchurColoring N c) if there are no $x, y \ge 1$ with $x + y \le N$ and $c(x) = c(y) = c(x + y)$ , the case $x = y$ included. The cover form uses SumFree S and CoveredBySumFree X n ( $X$ lies in the union of $n$ sumfree sets); for $n \ge 1$ the two bridge theorems pass between the two forms in both directions.

Triangle Ramsey property. $\mathrm{TR}(k, r)$ (TriangleRamsey k r): every colouring with at most $k$ colours of the pairs $x < y$ of a finite set of at least $r$ naturals has a monochromatic triangle. For $k \ge 1$ it is the inequality $R_k(3) \le r$ .

Neighbourhoods. The difference colouring gives a pair $\{x, y\}$ the colour $c(|x - y|)$ . For a Schur colouring of $[1, N]$ it has no monochromatic triangle on $[0, N]$ , since $(y - x) + (z - y) = z - x$ . Write

$\Gamma_i(V, v) = \{\, w \in V : w \ne v,\ c(|v - w|) = i \,\}$ (colorNbhd c V v i);
$V_m = \Gamma_{c(m+1)}([0, 2m+1], m)$ , the central neighbourhood (centralNbhd c m), which contains $2m + 1$ ;
$P_i = \Gamma_i(V_m, 2m+1)$ , the endpoint neighbourhoods (endpointNbhd c m i).

The frontier. The frontier hypotheses are $\mathrm{TR}(k, u + 1)$ , $2t = (k+1)u$ , $m = (k+2)t$ , and $c$ a Schur colouring of $[1, 2m + 1]$ with $k + 2$ colours. From the first two, $\mathrm{TR}(k + 1, 2t + 2)$ holds, and the centred bound excludes Schur colourings of $[1, 2m + 2]$ with $k + 2$ colours; $[1, 2m + 1]$ is the frontier interval. Six colours: $k = 4$ , $u = 60$ , $t = 150$ , $m = 900$ , $2m + 1 = 1801$ .

Example. For $k = 1$ , $u = 2$ , $t = 2$ , $m = 6$ (and $13 = S(3)$ ), the classes $\{1, 4, 7, 10, 13\}$ , $\{2, 3, 11, 12\}$ , $\{5, 6, 8, 9\}$ form a Schur colouring of $[1, 13]$ , with $V_6 = \{2, 5, 7, 10, 13\}$ and endpoint neighbourhoods $\{2, 10\}$ and $\{5, 7\}$ , both closed under $x \mapsto 12 - x$ .

Formalization targets

Goal: six colours under $R_4(3) \le 61$

\mathrm{TR}(4, 61) \ \text{ and } \ c \text{ a Schur colouring of } [1, 1801] \text{ with six colours} \implies (1)\text{–}(5),

where $q = c(901)$ , $V = V_{900}$ and $P_i = \Gamma_i(V, 1801)$ :

each colour occurs $150$ times in $[1, 900]$ ;
$|V| = 301$ ;
$|\Gamma_i(V, v)| = 60$ for every $v \in V$ and every colour $i \ne q$ ;
$c(901 - d) = c(901 + d)$ for every $d \in [1, 900]$ with $c(d) = q$ ;
for every colour $i \ne q$ : $|P_i| = 60$ ; $x \mapsto 1800 - x$ maps $P_i$ to itself without fixed points; and $c(|x - y|) \notin \{i, q\}$ for distinct $x, y \in P_i$ .

The goal is a structure theorem under the hypothesis $R_4(3) \le 61$ . It does not prove $S(6) \le 1800$ , and it does not assert that a Schur colouring of $[1, 1801]$ with six colours exists; whether such a colouring, or the structure it would force, exists is open. The goal is the six-colour instance of the general theorems below.

Centred-interval bound

\mathrm{TR}(k, r) \implies \Bigl[1,\ 2(k+1)\Bigl\lfloor \tfrac{r-1}{2} \Bigr\rfloor + 2\Bigr] \text{ is not covered by } k + 1 \text{ sumfree sets.}

Balanced colour classes

\mathrm{TR}(k, 2t + 2),\ m = (k+1)t,\ c \text{ a Schur colouring of } [1, 2m+1] \text{ with } k + 1 \text{ colours} \implies \bigl|\{\, d \in [1, m] : c(d) = j \,\}\bigr| = t \ \text{ for every colour } j.

Nested saturation

\text{frontier hypotheses} \implies |\Gamma_i(V_m, v)| = u \qquad (v \in V_m,\ i \ne c(m+1)).

Automorphism extension

For a colouring $\mathrm{col}$ of ordered pairs, a finite set $W$ , a point $e \notin W$ and a map $J$ with $J(W) \subseteq W$ , $J \circ J = \mathrm{id}$ on $W$ and $\mathrm{col}(J(x), J(y)) = \mathrm{col}(x, y)$ on $W$ :

v \in W \text{ and } J(v) \text{ have equal colour degrees in } W \cup \{e\} \implies \mathrm{col}(v, e) = \mathrm{col}(J(v), e).

Forced reflection

\text{frontier hypotheses} \implies c(m + 1 - d) = c(m + 1 + d) \qquad (d \in [1, m],\ c(d) = c(m+1)).

The saturation degree is even

\text{frontier hypotheses} \implies u \text{ is even}.

Significance

The result itself. Under $R_4(3) \le 61$ , $S(6) \le 1801$ , and the goal constrains a six-colour Schur colouring of $[1, 1801]$ as listed above. In particular, each of its five endpoint neighbourhoods is a set of $30$ pairs $\{900 - d, 900 + d\}$ whose difference colouring uses at most four colours, is invariant under $x \mapsto 1800 - x$ and, like that of every subset of $[0, 1801]$ , has no monochromatic triangle. So such a colouring yields five colourings of $K_{60}$ with at most four colours, no monochromatic triangle and a fixed-point-free colour-preserving involution. A proof that this configuration cannot occur would give $S(6) \le 1800$ under the same hypothesis. Whether it can occur, and whether $S(6) \le 1800$ , are open.

Formalizing it. All 12 theorems of the tree, the goal included, are proved in Lean 4 with Mathlib over the bundles ClassicalSchurBasic, ClassicalSchurRamsey and ClassicalSchurColoring, with the axioms propext, Classical.choice and Quot.sound only. Independent Claude agents checked the Lean: one rebuilt the frontier theorems, re-ran their axiom audit and checked their statements against the argument; another checked every statement of the tree against the mathematics. The mathematics is in the paper $S(6) \le 1801$ if $R_4(3) \le 61$ : a centred Schur bound and the structure at the frontier (A. McKenna, Zenodo, 2026, doi:10.5281/zenodo.23156099), and the Lean code is in its repository; the paper has not been refereed. $R_4(3) \le 61$ is not formalized in the mission.

Difficulty

The centred bound counts, for one colour class, the points $h \pm a$ around the centre of the interval. At the frontier every such count is tight: each colour has $t$ elements in $[1, m]$ , and inside $V_m$ each colour other than $c(m+1)$ has degree $u$ , the largest value that $R_k(3) \le u + 1$ allows. So no single counting step gives a contradiction, and the theorems describe the tight case instead of excluding it. The first exclusion that the structure gives, parity, works only for odd $u$ ; at six colours $u = 60$ .

The reflection is not a property of Schur colourings in general: the colouring $\{1, 4\}$ , $\{2, 3\}$ , $\{5\}$ of $[1, 5]$ has $c(2) = c(3)$ but $c(1) \ne c(5)$ . At the frontier the theorem asserts it only for the $d$ with $c(d) = c(m+1)$ , so an argument that assumes a fully symmetric colouring proves a different statement. A direct search is no substitute: $S(5) = 160$ already needed a large certified SAT computation (Heule 2018), and $[1, 1801]$ with six colours is a much larger instance.

Formalization scope

Colourings are functions ℕ → Fin n on all of $\mathbb{N}$ ; SchurColoring N c constrains only $[1, N]$ , with $x = y$ allowed. Distances are Nat.dist.
Neighbourhoods are Finsets. $V_m$ lies in range (2 * m + 2) $= [0, 2m+1]$ , so the point $0$ is a candidate member; the centre $m$ never is.
TriangleRamsey k r takes colours from any Finset of at most $k$ naturals; the pair colouring ℕ → ℕ → ℕ is constrained only on the pairs $x < y$ of the vertex set, which is any finite set of naturals. TriangleRamsey k 0 and TriangleRamsey k 1 are false.
Covers. CoveredBySumFree X n uses Fin n → Set ℕ; the sets need not be disjoint or lie in $X$ .
Subtraction is truncated. Under the hypotheses, none of $r - 1$ , $N - 1$ , $m + 1 - d$ , $2m - x$ (with $x \in P_i$ ), $901 - d$ and $1800 - x$ truncates.
No trivialization. The frontier theorems are vacuous for $u = 0$ , and for $k = 0$ (then $[1, 2m + 1] \supseteq [1, 5]$ , while $S(2) = 4$ ). For $k = 1$ they are not: the Schur colourings of $[1, 13]$ meet the hypotheses, and every conclusion can be checked by hand. The goal holds vacuously if $R_4(3) > 61$ or if no six-colour Schur colouring of $[1, 1801]$ exists; it is a structure theorem, not a claim that such a colouring exists.

Bundles: ClassicalSchurBasic (SumFree, CoveredBySumFree) and ClassicalSchurRamsey (TriangleRamsey) are already public; ClassicalSchurColoring holds SchurColoring, colorNbhd, centralNbhd and endpointNbhd. Reusable: the colouring–cover bridges, the pigeonhole step, the centred bound for every $k$ , and the automorphism-extension lemma (arbitrary types). Welcome beyond the targets: a formal proof of TriangleRamsey 4 61, and results on whether the configuration of five paired $60$ -point sets exists.

Provenance: the centred-interval argument was first written by an AI agent based on ChatGPT (OpenAI) in a project discussion on 2026-09-27, and a Claude (Anthropic) agent audited it. The balance, saturation and reflection argument was proposed by an AI agent based on ChatGPT (OpenAI) in a project discussion; Claude checked each step and restated it with explicit hypotheses. Claude wrote the Lean proofs of both parts; the independent checks are described under Formalizing it.

Selected references

R. E. Greenwood, A. M. Gleason, Combinatorial relations and chromatic graphs, Canad. J. Math. 7 (1955) 1–7. https://doi.org/10.4153/CJM-1955-001-4
S. W. Golomb, L. D. Baumert, Backtrack programming, J. ACM 12 (1965) 516–524. https://doi.org/10.1145/321296.321300
F. R. K. Chung, On the Ramsey numbers $N(3, 3, \dots, 3; 2)$ , Discrete Math. 5 (1973) 317–321. https://doi.org/10.1016/0012-365X(73)90125-8
H. Fredricksen, M. M. Sweet, Symmetric sum-free partitions and lower bounds for Schur numbers, Electron. J. Combin. 7 (2000) #R32. https://doi.org/10.37236/1510
M. J. H. Heule, Schur number five, Proc. AAAI Conf. Artif. Intell. 32 (2018). https://doi.org/10.1609/aaai.v32i1.12209 ; preprint arXiv:1711.08076 (2017). https://arxiv.org/abs/1711.08076
S. P. Radziszowski, Small Ramsey numbers, Electron. J. Combin., Dynamic Survey DS1, revision 18, 2026. https://doi.org/10.37236/21
M. Tatarevic, An improved upper bound for the Ramsey number R(3,3,3,3), GitHub repository, 2026, commit ddd7755. https://github.com/milostatarevic/r3333-upper-bound/commit/ddd7755476db3f0751181db0daec75342576cdd1
A. McKenna, $S(6) \le 1801$ if $R_4(3) \le 61$ : a centred Schur bound and the structure at the frontier, Zenodo, 2026. https://doi.org/10.5281/zenodo.23156099 ; Lean code: https://github.com/mysticflounder/schur-centred-bound (release v1.0.1).

15 thms1 active userReviewed

Operations Research Optimization·Captain: mikedeng1

Project Scheduling with Time Windows and Scarce Resources IV: Every Feasible Schedule Obeys a Minimal Delaying Mode of Each Forbidden SetTextbook

Motivation

Resource-constrained project scheduling with general temporal constraints, written $PS|temp|C_{\max}$ , asks for start times of the activities of a project that respect minimum and maximum time lags between activities and the capacities of renewable resources (staff, machines, reactors), and that minimize the project duration. Deciding whether a feasible schedule exists at all is already NP-complete (Bartusch, Möhring and Radermacher, 1988), so exact methods are branch-and-bound procedures. The dominant family, going back to De Reyck and Herroelen (1998) and presented in Chapter 2 of Neumann, Schwindt and Zimmermann's monograph, branches on resource conflicts: whenever the currently computed schedule overloads a resource at some time $t$ , the set of activities in progress at $t$ is a forbidden set, and the node is split into children, each of which adds precedence constraints that resolve the conflict.

Such a scheme is only correct if the children together retain every feasible schedule. Theorem 2.5.7 of the book is exactly this completeness guarantee, and it is the reason the enumeration can be restricted to the small family of minimal delaying modes instead of arbitrary ways of breaking up a conflict. The same section also contains the preprocessing results (§2.5.2) that exploit two-element forbidden sets before any branching happens. This mission formalizes both.

Setting

A project has activities $V=\{0,1,\dots,n+1\}$ with $n\ge1$ ; activity $0$ is the project beginning and $n+1$ the project completion, both of duration $0$ , and every real activity $i\in\{1,\dots,n\}$ has an integer duration $p_i>0$ . The project network $N$ has arc set $E$ and integer arc weights $\delta_{ij}$ ; the arc $\langle i,j\rangle$ imposes the temporal constraint $S_j-S_i\ge\delta_{ij}$ . A finite set $\mathcal R$ of renewable resources is given; resource $k$ has capacity $R_k\in\mathbb N$ and activity $i$ uses $r_{ik}\in\mathbb Z_{\ge0}$ units of it, with $r_{ik}\le R_k$ and $r_{0k}=r_{n+1,k}=0$ .

A schedule is a vector $S=(S_i)_{i\in V}$ of real start times with $S_0=0$ and $S_i\ge0$ . The active set at time $t$ is $\mathcal A(S,t)=\{i\in V\mid S_i\le t<S_i+p_i\}$ . The schedule is time-feasible if it satisfies all temporal constraints, resource-feasible if

\sum_{i\in\mathcal A(S,t)}r_{ik}\le R_k\qquad(k\in\mathcal R,\ t\ge0),

and feasible if it is both; $\mathcal S$ denotes the set of feasible schedules.

A set $F\subseteq V$ is forbidden if $\sum_{i\in F}r_{ik}>R_k$ for some $k$ , a feasible set otherwise, and minimal forbidden if no proper subset is forbidden. For a forbidden $F$ , a set $B\subseteq F$ is a delaying alternative if $F\setminus B$ is feasible, and a minimal delaying alternative if no proper subset of $B$ is one. A minimal delaying mode for $F$ is a pair $(i,B)$ with $B$ a minimal delaying alternative for $F$ and $i\in F\setminus B$ .

For §2.5.2, fix an integer upper bound $UB$ on the project duration. The temporal scheduling network $N^+$ adds to $N$ the arc $\langle n+1,0\rangle$ with weight $\delta_{n+1,0}=-UB$ , and $d_{ij}$ is the longest path length from $i$ to $j$ in $N^+$ ( $-\infty$ if there is no path, $d_{ii}=0$ ).

Formalization targets

Goal: Theorem 2.5.7 (p. 49)

For every forbidden set $F$ and every feasible schedule $S\in\mathcal S$ there is a minimal delaying mode $(i,B)$ for $F$ with

S_j\ge S_i+p_i\qquad(j\in B).

$F$ is arbitrary (not necessarily minimal); $B$ must be a minimal delaying alternative and $i$ must lie outside $B$ .

Milestones

Eqs. (2.5.2)–(2.5.3), p. 46. $B$ is a minimal delaying alternative for a forbidden $F$ iff $F\setminus B$ is a maximal feasible subset of $F$ , iff $B\subseteq F$ ,

\sum_{i\in F\setminus B}r_{ik}\le R_k\ (k\in\mathcal R)\quad\text{and}\quad\forall j\in B\ \exists k:\ \sum_{i\in F\setminus B}r_{ik}+r_{jk}>R_k.

Bartusch et al.'s criterion (proof of Theorem 2.3.10, p. 35). A schedule is resource-feasible iff every minimal forbidden set $F$ contains distinct $i,j$ with $S_j\ge S_i+p_i$ .
Lemma 2.5.5, p. 49. A minimal delaying alternative for $F$ is an inclusion-minimal set meeting every minimal forbidden $F'\subseteq F$ .
Theorem 2.5.11, p. 55. If $\{i,j\}$ is a two-element forbidden set with $d_{ij}<p_i$ and $d_{ij}>-p_j$ , then every feasible $S$ with $S_{n+1}\le UB$ satisfies $S_j\ge S_i+p_i$ .
Eq. (2.5.7), p. 55. If for a two-element forbidden set $\{i,j\}$ neither $d_{ij}>-p_j$ nor $d_{ji}>-p_i$ holds, then for all $h,l\in V$ and every feasible $S$ with $S_{n+1}\le UB$ ,

S_l\ge S_h+\min\bigl(d_{hi}+p_i+d_{jl},\ d_{hj}+p_j+d_{il}\bigr).

Significance

The result. Theorem 2.5.7 is the completeness statement of the De Reyck–Herroelen enumeration scheme (Algorithm 2.5.8): if every child of a conflict node imposes the precedence constraints $i\to j$ ( $j\in B$ ) of one minimal delaying mode $(i,B)$ , the children's order polyhedra together contain all feasible schedules of the parent. Proposition 2.5.9(a), the correctness of the whole branch-and-bound procedure, rests on it. Because the objective does not enter, the book reuses the theorem for the regular and nonregular objectives of Chapter 3. Theorem 2.5.11 and inequality (2.5.7) are the preprocessing rules that shrink the time-feasible region before enumeration: each adds temporal constraints that every feasible schedule within the bound already satisfies, which raises the lower bound $ES_{n+1}$ and prunes the enumeration.

Formalizing it. All statements are proved in the book (Bartusch et al.'s criterion is quoted from their 1988 paper with the necessity argument sketched). None of them has a machine-checked proof; the Prove2Me catalog contains precedence-only scheduling models (Brucker–Knust) and acyclic event networks (Kelley–Walker) but no model with time windows and forbidden sets. The mission produces a reusable library of forbidden sets, delaying alternatives and longest-path distances in networks with maximum time lags.

Difficulty

The obvious idea — pick any two overlapping activities and delay one — does not give a minimal delaying alternative with a single delaying activity $i$ common to all of $B$ . The proof has to pass from the pairwise separations that resource-feasibility guarantees in each minimal forbidden subset to a set $B$ that is simultaneously minimal as a delaying alternative and ordered behind one activity outside $B$ . This needs the correspondence between delaying alternatives and hitting sets of the minimal forbidden subsets (Lemma 2.5.5) and the positivity of real durations to keep $i$ outside $B$ . For the preprocessing results, the delicate part is relating longest paths in $N^+$ , including the backward arc carrying $-UB$ , to the start-time differences of every feasible schedule within the bound.

Formalization scope

Activities are Fin (n + 2), with $n+1$ as Fin.last (n + 1). Start times are real; durations, capacities, requirements and time lags are integers (natural numbers where the book says so). The standing assumptions of the book (at least one real activity, zero-duration dummies, positive durations of real activities, no loops, $r_{0k}=r_{n+1,k}=0$ , $r_{ik}\le R_k$ , and paths in $N$ from $0$ to every node and from every node to $n+1$ ) are one hypothesis P.StandingAssumptions of every theorem.

Resource constraints are imposed for every $t\ge0$ , not only for $0\le t\le\bar d$ as (2.1.4) literally writes. The book's proofs and Remark 2.3.11 use the $t\ge0$ reading; with the literal cut-off, schedules running past $\bar d$ could violate capacities after $\bar d$ , and Bartusch et al.'s criterion would fail.

Longest path lengths are maxima over simple paths, with values in WithBot ℝ (⊥ for $-\infty$ ). If $N^+$ has a cycle of positive length, no schedule satisfies the temporal constraints with $S_{n+1}\le UB$ , and the statements using $d_{ij}$ are vacuous, as in the book. The arc $\langle n+1,0\rangle$ of $N^+$ has weight $-UB$ , or $\max(\delta_{n+1,0},-UB)$ if $N$ already has such an arc. $UB$ is an integer.

The goal is not trivial: it quantifies over minimal delaying modes only. A variant without the minimality of $B$ , or allowing $i\in B$ , would be nearly empty (take $B=F\setminus\{i\}$ ), and the statement here rules both out. Maximality in milestone 1 is taken among subsets of $F$ .

Welcome contributions: the hitting-set correspondence between delaying alternatives and minimal forbidden subsets, the telescoping bound $S_j-S_i\ge d_{ij}$ for feasible schedules, and proofs of any milestone. The definitions restate the setup of the series' earlier missions (II: order polyhedra) locally, because those are still drafts.

Selected references

K. Neumann, C. Schwindt, J. Zimmermann, Project Scheduling with Time Windows and Scarce Resources, 2nd ed., Springer, 2003, §2.5. https://doi.org/10.1007/978-3-540-24800-2
M. Bartusch, R. H. Möhring, F. J. Radermacher, Scheduling project networks with resource constraints and time windows, Annals of Operations Research 16 (1988) 201–240. https://doi.org/10.1007/BF02283745
B. De Reyck, W. Herroelen, A branch-and-bound procedure for the resource-constrained project scheduling problem with generalized precedence relations, European Journal of Operational Research 111 (1998) 152–174. https://doi.org/10.1016/S0377-2217(97)00305-6

8 thms1 active userReviewed

Graph Theory Operations Research Optimization·Captain: mikedeng1

Project Scheduling with Time Windows and Scarce Resources II: A Time-Feasible Strict Order Is Feasible iff It Breaks Up Every Minimal Forbidden SetTextbook

Motivation

Resource-constrained project scheduling asks for start times of the activities of a project so that prescribed time lags between activities are respected and, at every moment, the activities in progress do not require more of any renewable resource (staff, machines, reactors) than is available. When the time lags include maximum time lags (deadlines relative to other activities), even finding a feasible schedule is NP-hard, and the feasible region is in general neither convex nor connected. Branch-and-bound methods for this problem (the problem $PS|temp|C_{\max}$ in the notation of Neumann, Schwindt & Zimmermann) do not search over schedules directly. They search over strict orders of the activities, that is, over sets of precedence constraints " $j$ starts after $i$ has finished".

This mission formalizes the theory behind that search, as developed by Bartusch, Möhring & Radermacher (1988) and presented in §2.3 of Neumann, Schwindt & Zimmermann, Project Scheduling with Time Windows and Scarce Resources (2nd ed., Springer 2003). Its goal, Theorem 2.3.10, says when a strict order resolves every resource conflict.

Setting

A project has activities $V = \{0, 1, \dots, n+1\}$ , where $0$ and $n+1$ are fictitious activities marking the project's start and completion and $1, \dots, n$ are the real activities ( $n \ge 1$ ). Activity $i$ has duration $p_i \in \mathbb Z_{\ge 0}$ , with $p_0 = p_{n+1} = 0$ and $p_i > 0$ for real activities. Time lags are encoded in the project network $N$ : an arc $\langle i, j\rangle \in E$ with integer weight $\delta_{ij}$ imposes $S_j - S_i \ge \delta_{ij}$ . The book's standing assumptions give, for every node $i$ , a path from $0$ to $i$ of nonnegative length and a path from $i$ to $n+1$ of length at least $p_i$ .

A schedule is a vector $S \in \mathbb R^{n+2}$ with $S_0 = 0$ and $S_i \ge 0$ . It is time-feasible if $S_j - S_i \ge \delta_{ij}$ for all arcs. The set of time-feasible schedules is $\mathcal S_T$ .

Each renewable resource $k \in \mathcal R$ has a capacity $R_k$ , and activity $i$ uses $r_{ik} \le R_k$ units of it while in progress, with $r_{0k} = r_{n+1,k} = 0$ . The active set at time $t$ is $\mathcal A(S,t) = \{ i \mid S_i \le t < S_i + p_i\}$ , and $S$ is resource-feasible if $\sum_{i \in \mathcal A(S,t)} r_{ik} \le R_k$ for all $k$ and all $t \ge 0$ . The feasible region $\mathcal S$ consists of the schedules that are both time-feasible and resource-feasible.

A strict order $O \subseteq V \times V$ is an asymmetric, transitive relation. Its order polyhedron is

\mathcal S_T(O) = \{ S \in \mathcal S_T \mid S_j \ge S_i + p_i \ \text{for all } (i,j) \in O\}.

$O$ is time-feasible if $\mathcal S_T(O) \ne \emptyset$ , and feasible if moreover $\mathcal S_T(O) \subseteq \mathcal S$ . The order network $N(O)$ adds to $N$ , for each $(i,j) \in O$ , an arc $\langle i,j\rangle$ of weight $p_i$ , or raises the weight of an existing arc to $\max(\delta_{ij}, p_i)$ . A schedule $S$ induces the strict order $O(S) = \{(i,j) \mid i \ne j,\ S_j \ge S_i + p_i\}$ .

A set $F \subseteq V$ is forbidden if $\sum_{i \in F} r_{ik} > R_k$ for some resource $k$ . It is a minimal forbidden set if no proper subset of it is forbidden. $\mathcal F$ denotes the set of minimal forbidden sets.

Formalization targets

Goal: Theorem 2.3.10 (Bartusch et al. 1988)

For every time-feasible strict order $O$ ,

O \text{ feasible} \iff \forall F \in \mathcal F\ \exists\, i, j \in F:\ N(O) \text{ has a path from } i \text{ to } j \text{ of length} \ge p_i .

Milestones

Proposition 2.3.3. A strict order $O$ is time-feasible if and only if $N(O)$ has no cycle of positive length.
Bartusch et al.'s criterion (quoted in the proof of Theorem 2.3.10). A schedule $S$ is resource-feasible if and only if every $F \in \mathcal F$ contains distinct $i, j$ with $S_j \ge S_i + p_i$ .
Proposition 2.3.6. For time-feasible $S$ , the strict order $O(S)$ is feasible if and only if $S \in \mathcal S$ .
Theorem 2.3.7. $\mathcal S = \bigcup_{O \in \mathcal O} \mathcal S_T(O)$ , where $\mathcal O$ is the finite set of inclusion-minimal feasible strict orders.
Remark 2.3.11. A time-feasible schedule partitions $F$ if and only if every $\mathcal A(S,t) \cap F$ , $t \ge 0$ , is feasible. A time-feasible order is feasible if and only if it breaks up all (equivalently, all minimal) forbidden sets. A time-feasible schedule is feasible if and only if it partitions all forbidden sets.

Significance

Theorem 2.3.10 turns the feasibility of a strict order, which is a statement about infinitely many schedules and all times $t$ , into a finite check: one longest-path computation in $N(O)$ for each minimal forbidden set. Together with Proposition 2.3.3 and the structural Theorem 2.3.7, it shows that $\mathcal S$ is a finite union of polyhedra indexed by feasible strict orders. This justifies the enumeration schemes of Chapter 2 of the book (branching on the pairs that break up a minimal forbidden set) and the notions of active and stable schedules developed in later sections.

All results in this mission are proved in the literature. For the resource-feasibility criterion, the book cites Bartusch et al. (1988) instead of proving it. To our knowledge, none of these results has been machine-checked. A formal development would give a verified foundation for the order-based description of the feasible region, on which later missions of this series (active schedules, delaying modes, stable schedules) build.

Difficulty

The sufficiency half of the goal is short once the criterion is available: a path of length $\ge p_i$ in $N(O)$ forces $S_j \ge S_i + p_i$ on the whole order polyhedron. The necessity half carries the content. If for some minimal forbidden set $F$ no path in $N(O)$ between elements of $F$ reaches the required length, one must construct a schedule in $\mathcal S_T(O)$ in which all activities of $F$ are simultaneously in progress. This means adding the reverse constraints $S_j - S_i < p_i$ for all $i, j \in F$ to the temporal system without creating a cycle of positive length, while keeping $S_0 = 0$ and $S \ge 0$ . The obvious reading "no single arc gives a precedence, so they can overlap" fails because maximum time lags combine into long paths through activities outside $F$ . The standing assumption that every node is reachable from $0$ by a path of nonnegative length is needed here: without it the equivalence is false.

Formalization scope

The activity set is Fin (n + 2): 0 is the project start and Fin.last (n + 1) the project completion. Durations and resource data are natural numbers, arc weights are integers, and start times are real numbers.
Strict orders are finite sets of pairs, Finset (Fin (n+2) × Fin (n+2)), required to be asymmetric and transitive.
Resource constraints hold for every $t \ge 0$ . The book's (2.1.4) writes $0 \le t \le \bar d$ . In Chapter 2 schedules are not bounded by $\bar d$ , and the book's proofs and Remark 2.3.11 use all $t \ge 0$ . This is a convention of the whole series, not a strengthening.
A path is a walk (nodes may repeat) and its length is the sum of its arc weights. A cycle of positive length is a closed walk with at least one arc and positive length. For a time-feasible order, $N(O)$ has no cycle of positive length. In that case "some path of length $\ge p_i$ " coincides with the book's "longest path length $\ge p_i$ ", so no supremum over paths appears.
The standing assumptions of the book form a single predicate Project.StandingAssumptions, which is a hypothesis of every theorem: $n \ge 1$ ; $p_0 = p_{n+1} = 0$ and $p_i > 0$ otherwise; no loops; $r_{0k} = r_{n+1,k} = 0$ and $r_{ik} \le R_k$ ; and the two path conditions of p. 8.
Minimal forbidden sets and inclusion-minimal feasible orders use Mathlib's Minimal, taken among forbidden sets and among feasible strict orders respectively.
The goal is an equivalence, and both directions are required. Weakening it to sufficiency, or dropping the time-feasibility of $O$ or the minimality of $F$ , would change the theorem. Keeping the book's cut-off $t \le \bar d$ would also change it, because a schedule could then have an unresolved conflict after $\bar d$ and still be called feasible.
Theorem 1.3.3 of Chapter 1 (a time-feasible schedule exists if and only if the network has no cycle of positive length) is needed for Proposition 2.3.3 and is restated here for $N(O)$ . Chapter 1's mission is drafted separately.
Useful infrastructure beyond this mission: longest-path potentials on integer-weighted digraphs without positive cycles (feasibility of difference constraints), and the walk and cycle API on Network. Contributions of this general lemma layer are welcome.

Selected references

K. Neumann, C. Schwindt, J. Zimmermann, Project Scheduling with Time Windows and Scarce Resources, 2nd ed., Springer, 2003. https://doi.org/10.1007/978-3-540-24800-2
M. Bartusch, R. H. Möhring, F. J. Radermacher, Scheduling project networks with resource constraints and time windows, Annals of Operations Research 16 (1988), 201–240. https://doi.org/10.1007/BF02283745

9 thms1 active userReviewed

Algorithmic Game Theory Mechanism Design Operations Research·Captain: mikedeng1

An Introduction to the Theory of Mechanism Design IX: Monotone Direct Mechanisms Are Dictatorial (Gibbard–Satterthwaite)Textbook

Motivation

Voting rules, committee procedures and any other method that turns individual rankings into one collective choice face the same question: can the rule be designed so that no participant ever gains by misreporting their ranking? The Gibbard–Satterthwaite theorem (Gibbard, 1973; Satterthwaite, 1975) answers no. When at least three alternatives can be chosen and all strict rankings are admissible, the only rules immune to manipulation are dictatorships. The result is the starting point of mechanism design without money. It explains why the positive results of the transferable-utility chapters of the book (Groves, VCG, posted prices) depend on quasi-linear preferences, and why research on voting turned to restricted preference domains and weaker solution concepts.

This mission formalizes Chapter 8 of Börgers, An Introduction to the Theory of Mechanism Design (Oxford University Press, 2015), §§8.2–8.3. The book's route to the theorem follows Reny (2001). Strategy-proofness implies Maskin monotonicity, and every monotone rule with full range over at least three alternatives is dictatorial. The second step is the Muller–Satterthwaite theorem (Muller and Satterthwaite, 1977), which is stronger than Gibbard–Satterthwaite because monotonicity is weaker than strategy-proofness. The chapter closes with the classical escape route: on single-peaked preferences (Moulin, 1980) the median voting rule is strategy-proof and not dictatorial.

Timeline. Arrow (1951/1963) proved the impossibility of non-dictatorial preference aggregation under independence of irrelevant alternatives. Gibbard (1973) and Satterthwaite (1975) proved the manipulation version independently, and Satterthwaite showed the two theorems are equivalent. Muller and Satterthwaite (1977) showed that on the full domain strategy-proofness is equivalent to a monotonicity condition (strong positive association). Moulin (1980) characterized strategy-proof rules on single-peaked domains that depend only on reported peaks. Reny (2001) gave the short common proof of Arrow's and the Muller–Satterthwaite theorems that the book follows.

Setting

There is a finite set $I=\{1,\dots,N\}$ of agents and a finite set $A$ of alternatives. Each agent $i$ has a preference relation $R_i$ over $A$ ; $a\,R_i\,b$ reads " $a$ is weakly preferred to $b$ ". Every $R_i$ is a linear order: complete, transitive, and the only indifference is among identical alternatives. Its strict part is $P_i$ . The set of all linear orders over $A$ is $\mathcal R$ , and a profile is $R=(R_1,\dots,R_N)\in\mathcal R^N$ . $(R_i',R_{-i})$ is the profile obtained from $R$ by replacing agent $i$ 's preference with $R_i'$ .

A direct mechanism is a function $f:\mathcal R^N\to A$ (Definition 8.1). It is

dominant strategy incentive-compatible (DSIC) if $f(R_i,R_{-i})\,R_i\,f(R_i',R_{-i})$ for all $i$ , $R$ , $R_i'$ (Definition 8.2);
dictatorial if some agent $i$ satisfies $f(R)\,R_i\,a$ for all profiles $R$ and all $a\in A$ (Definition 8.3);
monotone if $f(R)=a$ and, for every $i$ , $a\,R_i\,b\Rightarrow a\,R_i'\,b$ for all $b$ , together imply $f(R')=a$ (Definition 8.4);
set-monotone if $f(R)\in B$ and, for every $i$ , $R_i'$ differs from $R_i$ only in the ranking of elements of $B$ , together imply $f(R')\in B$ (Definition 8.5);
unanimity-respecting if $f(R)=a$ whenever every agent ranks $a$ at the top (Definition 8.6).

"The range of $f$ is $A$ " means that every alternative is chosen at some profile.

For §8.3 the alternatives are labelled $1,\dots,K$ . A preference is single-peaked if it has a top alternative $k(i)$ and declines monotonically to the right and to the left of it. $\hat{\mathcal R}$ is the set of single-peaked preferences, and on the restricted domain $\hat{\mathcal R}^N$ DSIC and dictatorship are read with all profiles and deviations taken from $\hat{\mathcal R}$ .

Formalization targets

Goal: Proposition 8.5 (Muller–Satterthwaite)

|A|\ge 3,\quad f(\mathcal R^N)=A,\quad f\ \text{monotone}\ \Longrightarrow\ \exists\, i\in I\ \ \forall R\in\mathcal R^N\ \forall a\in A:\ f(R)\,R_i\,a.

This is the book's own capstone ("the core of the proof", p.144). No constant needs to be fixed, and the statement is strictly stronger than the necessity half of Gibbard–Satterthwaite.

Milestones

Proposition 8.2: DSIC $\Rightarrow$ monotone.
Proposition 8.3: monotone $\Rightarrow$ set-monotone.
Proposition 8.4: monotone and full range $\Rightarrow$ respects unanimity.
Proposition 8.1 (Gibbard–Satterthwaite): for $|A|\ge3$ and full range, $f$ is DSIC $\iff$ $f$ is dictatorial.
Proposition 8.6: for $|A|\ge3$ and at least two agents, there is a mechanism on $\hat{\mathcal R}^N$ with range $A$ that is DSIC on $\hat{\mathcal R}^N$ and not dictatorial on $\hat{\mathcal R}^N$ .

Significance

The result itself. Proposition 8.5 turns an incentive question into a purely ordinal one: any full-range rule that is Maskin monotone is a dictatorship once three alternatives are available. With Proposition 8.2 it gives Gibbard–Satterthwaite. Proposition 8.6 marks the boundary of the impossibility: with a one-dimensional ordering of alternatives and single-peaked preferences, the median voter rule escapes it.

Formalizing it. All results are classical and proved. The platform already has a proved Gibbard–Satterthwaite theorem (AGT.gibbard_satterthwaite, Algorithmic Game Theory III), derived from Arrow's theorem in the alternative Mathlib environment c5ea0035…. It uses strict-order profiles and a one-agent-deviation monotonicity. This mission adds Maskin monotonicity, the Muller–Satterthwaite theorem, Reny's direct proof route, and the single-peaked possibility result, none of which is on the platform, all in the default environment.

Difficulty

Propositions 8.2–8.4 are short. The difficulty is in Proposition 8.5. Its proof moves one alternative up or down agents' rankings one agent at a time, and it has to keep the chosen alternative pinned at every step using only monotonicity, set-monotonicity and unanimity. It needs a pivotal agent, whose identity depends on the pair of alternatives, and then an argument that the pivots for different alternatives coincide. The argument uses a third alternative $c$ in an essential way. With two alternatives the conclusion is false (majority rule), so any argument that never uses $|A|\ge3$ cannot succeed. Formally, each "move $b$ just below $a$ in agent $j$ 's ranking" is an explicit construction of a new linear order, together with a check that the monotonicity hypothesis applies. The figures on pp.146–149 describe these orders only partially ("the other alternatives in arbitrary order"). For Proposition 8.6, the obstacle is that DSIC must be checked against every single-peaked misreport, not only misreports of the peak.

Formalization scope

A linear order is the structure LinPref A (relation rel, completeness, transitivity, antisymmetry). A profile is ι → LinPref A for a finite agent type ι, and a direct mechanism is (ι → LinPref A) → A. $A$ is a Fintype. "The range of $f$ is $A$ " is Function.Surjective f, and $|A|\ge3$ is 3 ≤ Fintype.card A.
Monotonicity is the book's Definition 8.4 for arbitrary pairs of profiles, with the lower-contour condition required for each agent separately. Dictatorship is ∃ i, ∀ R a, f R ≥_{R_i} a, with the agent chosen before the profile. A weaker monotonicity (one-agent deviations only) or a weaker dictatorship ("some agent's top is chosen at some profile") would trivialize the goal and is ruled out.
§8.3: the labelling is lab : A ≃ Fin K (labels $0,\dots,K-1$ ). The restricted domain is a predicate on LinPref A, and DSIC, dictatorship and full range are relativized to profiles in the domain (IsDSICOn, IsDictatorialOn, HasFullRangeOn). Values of the mechanism off the domain are never consulted.
Two corrections of the page. The left-hand clause of single-peakedness is printed as $(\ell-1)\,R_i\,\ell$ and is used as $\ell\,R_i\,(\ell-1)$ (the book's words "decline monotonically to the left"). Proposition 8.6 carries the added hypothesis $N\ge2$ , since with one agent every onto strategy-proof rule is dictatorial.
Proposition 8.6 is an existence statement. The median voting mechanism is the book's witness, but the statement does not fix it.
Reusable beyond this mission: the linear-order profile model, Maskin monotonicity and the restricted-domain notions, which apply to Arrow-type results, implementation theory and Moulin's characterization. Proofs of any milestone, or an independent formal proof of Proposition 8.5, are welcome.

Selected references

T. Börgers, An Introduction to the Theory of Mechanism Design, Oxford University Press, 2015, Ch. 8. https://doi.org/10.1093/acprof:oso/9780199734023.001.0001
A. Gibbard, "Manipulation of voting schemes: a general result", Econometrica 41 (1973) 587–601. https://doi.org/10.2307/1914083
M. A. Satterthwaite, "Strategy-proofness and Arrow's conditions", Journal of Economic Theory 10 (1975) 187–217. https://doi.org/10.1016/0022-0531(75)90050-2
E. Muller and M. A. Satterthwaite, "The equivalence of strong positive association and strategy-proofness", Journal of Economic Theory 14 (1977) 412–418. https://doi.org/10.1016/0022-0531(77)90140-5
P. J. Reny, "Arrow's theorem and the Gibbard–Satterthwaite theorem: a unified approach", Economics Letters 70 (2001) 99–105. https://doi.org/10.1016/S0165-1765(00)00332-3
H. Moulin, "On strategy-proofness and single peakedness", Public Choice 35 (1980) 437–455. https://doi.org/10.1007/BF00128122
S. Barberà, "An introduction to strategy-proof social choice functions", Social Choice and Welfare 18 (2001) 619–653. https://doi.org/10.1007/s003550100151

8 thms1 active userReviewed

Graph Theory Linear Optimization Operations Research+1·Captain: mikedeng1

Linear Programming: Foundations and Extensions III: Network Flows, the Integrality Theorem and König's TheoremTextbook

Motivation

Minimum-cost network flow problems are the largest special class of linear programs met in practice: transportation, distribution, assignment, communication and electric networks, facility location and financial planning all reduce to moving material along the arcs of a directed network from supply nodes to demand nodes at least cost. Chapter 14 of R. J. Vanderbei's Linear Programming: Foundations and Extensions (4th ed., Springer 2014, DOI 10.1007/978-1-4614-7630-6) develops the network simplex method, and closes with two structural facts that explain why this class is special: simplex bases are spanning trees of the network, and a network problem with integer supplies has integer basic solutions. Vanderbei then uses integrality to prove a classical theorem of combinatorics, König's theorem on regular bipartite graphs. Chapter 15, §5 treats the maximum-flow problem on the same objects and proves the Max-Flow Min-Cut Theorem.

The combinatorial results are older than linear programming. D. König proved in 1916 that every regular bipartite graph has a perfect matching (Math. Ann. 77). The Max-Flow Min-Cut Theorem is due to Ford and Fulkerson (1956, Canad. J. Math. 8) and, independently, Elias, Feinstein and Shannon (1956). The integrality of network bases is the total unimodularity of incidence matrices, known since the 1950s (Hoffman and Kruskal, 1956).

Setting

A network $(N,A)$ has a finite set $N$ of $m$ nodes and a set of directed arcs $A\subseteq\{(i,j): i,j\in N,\ i\ne j\}$ . Node $i$ carries a supply $b_i$ (negative values are demands) with $\sum_i b_i=0$ , and arc $(i,j)$ carries a cost $c_{ij}$ . The flow $x_{ij}$ on arc $(i,j)$ is the decision variable. The node–arc incidence matrix $A$ has in the column of $(i,j)$ an entry $+1$ in row $j$ , $-1$ in row $i$ , and $0$ elsewhere. The network flow problem (14.1) is

\text{minimize } c^{T}x\quad\text{subject to}\quad Ax=-b,\ x\ge 0 .

A flow satisfying $Ax=-b$ is balanced; a balanced flow with $x\ge0$ is feasible. Paths ignore arc directions; the network is connected if every two nodes are joined by a path, which is assumed throughout Chapter 14. A spanning tree is a set of arcs that, on all of $N$ and without directions, is connected and has no cycle. Fixing a root node $r$ and deleting its row gives the matrix $\tilde A$ . A set $T$ of arcs is a basis if its columns form an invertible square submatrix of $\tilde A$ , and a basic feasible solution is a feasible flow vanishing off some basis.

For maximum flow, a source $s$ , a sink $t$ and finite upper bounds $u_{ij}$ are given; all $b_i=0$ and an extra arc $(t,s)$ of infinite capacity is added. A feasible flow satisfies $0\le x_{ij}\le u_{ij}$ , $x_{ts}\ge0$ and flow balance. A cut is a node set $C$ with $s\in C$ , $t\notin C$ , and its capacity is $\kappa(C)=\sum_{(i,j)\in A,\ i\in C,\ j\notin C}u_{ij}$ .

Formalization targets

Goal: König's Theorem (Theorem 14.3, p. 216)

If $n$ girls and $n$ boys are such that every girl knows exactly $k\ge1$ boys and every boy knows exactly $k$ girls (knowing being symmetric), then there is a bijection $\sigma$ from girls to boys with

\text{girl } i \text{ knows boy } \sigma(i)\qquad\text{for all } i .

Milestones

Theorem 14.1 (p. 205): for a connected network, a set $T$ of arcs indexes a basis of $\tilde A$ if and only if $T$ is a spanning tree.
Theorem 14.2, Integrality Theorem (p. 216): with integer supplies, every basic feasible solution is integral,

x_{ij}\in\mathbb Z\qquad\text{for all }(i,j)\in A .

Eq. (15.8) (p. 234): $x_{ts}\le\kappa(C)$ for every feasible flow and every cut.
Theorem 15.1, Max-Flow Min-Cut (p. 234):

\max\{x_{ts}\}=\min_C \kappa(C),

both extrema attained.

The goal is independent of the network definitions in its statement; the milestones are the book's route to it (14.1, 14.2) and the chapter's other duality theorem on the same objects (15.8, 15.1).

Significance

König's theorem is the base case of matching theory: it gives perfect matchings in regular bipartite graphs, hence edge colourings of bipartite graphs with $\Delta$ colours, and via Birkhoff–von Neumann-type arguments the decomposition of doubly stochastic matrices. The Integrality Theorem is the reason assignment, transportation and shortest-path problems can be solved as linear programs without an integrality constraint. Theorem 14.1 is the correspondence the network simplex method is built on. Max-Flow Min-Cut is the prototype of combinatorial min–max theorems.

All four theorems are classical and proved. This mission adds machine-checked versions in the book's own formulation: the incidence matrix with Vanderbei's sign convention $Ax=-b$ , bases as square submatrices of $\tilde A$ with a chosen root, and maximum flow as a circulation through an added return arc. The platform already has network integrality, a tree-solution characterisation and max-flow min-cut in the Bertsimas–Tsitsiklis formulation and a Keller–Trotter max-flow statement; none is stated in this form, and Mathlib has Hall's marriage theorem but no regular-bipartite corollary.

Difficulty

The combinatorial content is small; the difficulty is in the passage between matrices and graphs. Theorem 14.1 needs both directions: the book shows that a spanning tree gives a triangularisable, hence invertible, submatrix and leaves the converse (independent columns form a spanning tree) as an exercise, which requires showing that any cycle, including a pair of antiparallel arcs, yields a linearly dependent set of columns and that $m-1$ acyclic arcs span. The book's proof of König's theorem applies the Integrality Theorem to the girl–boy network, which need not be connected, while Chapter 14 assumes connectedness throughout: the statement of 14.2 does not apply to it verbatim. The step "a feasible problem has a basic optimal solution" is also used and is not stated in the chapter.

Formalization scope

Nodes are a Fintype with decidable equality; arcs are a Finset (N × N), so parallel arcs are excluded as in the book, and IsNetwork excludes loops. Flows are real functions on ordered pairs; only their values on arcs matter.
"Connected" is preconnectedness of the undirected simple graph of the arcs; a spanning tree is an arc set whose undirected graph is a tree and in which no two arcs join the same pair of nodes.
A basis is $m-1$ linearly independent columns of the $(m-1)$ -row matrix $\tilde A$ , the same as an invertible square submatrix. The root $r$ is arbitrary, as in the book ("say, the last one").
Integer data means integer supplies; costs do not enter Theorem 14.2, since a basic optimal solution is a basic feasible solution.
In König's theorem both sides are Fin n, knowing is one relation between girls and boys, and $k\ge1$ is a hypothesis: the book's proof divides by $k$ , and for $k=0<n$ the claim is false. No connectedness is assumed.
For maximum flow, the return arc $(t,s)$ is a separate variable; $s\ne t$ and $u_{ij}\ge0$ are hypotheses that the book leaves implicit. Maximum and minimum are stated with attainment.
No statement involves a constant the book leaves implicit.

A formalization of the goal as a matching of size $n$ in some larger graph, or with the degree conditions on one side only, would be a different theorem; the conclusion is a bijection between exactly the $n$ girls and the $n$ boys using only acquainted pairs.

Useful infrastructure, reusable beyond this mission: the incidence matrix and its total unimodularity, the undirected graph of an arc set. Proofs of König's theorem through Hall's theorem (Mathlib Finset.all_card_le_biUnion_card_iff_exists_injective) are welcome alongside the book's route.

Selected references

R. J. Vanderbei, Linear Programming: Foundations and Extensions, 4th ed., Springer, 2014. DOI 10.1007/978-1-4614-7630-6
D. König, Über Graphen und ihre Anwendung auf Determinantentheorie und Mengenlehre, Math. Ann. 77 (1916), 453–465. DOI 10.1007/BF01456961
L. R. Ford and D. R. Fulkerson, Maximal flow through a network, Canad. J. Math. 8 (1956), 399–404. DOI 10.4153/CJM-1956-045-5
A. J. Hoffman and J. B. Kruskal, Integral boundary points of convex polyhedra, in Linear Inequalities and Related Systems, Ann. of Math. Studies 38, Princeton University Press, 1956, 223–246.

7 thms1 active userReviewed

Discrete Geometry Operations Research Optimization·Captain: Shuze Chen

Discrete Convex Analysis XIV: The König-Egerváry Theorem for Mixed MatricesTextbook

Motivation

Every physical or engineering model built from linear relations mixes two kinds of numbers. Some coefficients are exact — the $\pm 1$ entries recording Kirchhoff's current and voltage laws in an electrical network, or the incidence structure of a mechanical linkage — because they come from a topological or combinatorial fact, not a measurement. Others are physical parameters: resistances, masses, spring constants, reaction rates. These are known only approximately, and different parameters are, for modeling purposes, independent of one another. Classical linear algebra treats every entry of a coefficient matrix alike, so it cannot express this distinction, and a numerical computation on a matrix with noisy parameter entries can accidentally hit a non-generic coincidence — a determinant that would vanish only for a measure-zero set of parameter values, but that plain Gaussian elimination has no way to certify is not actually structurally forced to vanish. Murota and collaborators (see the bibliographical notes to chapter 12; the underlying theory is developed at length in Murota's Matrices and Matroids for Systems Analysis, 2000) formalized this distinction through mixed matrices, and showed that their key structural questions — is the matrix nonsingular, and what is its rank — reduce to a combinatorial optimization problem solvable by the discrete convex analysis this book develops. This mission formalizes that reduction and its capstone consequence, a generalization of the classical König–Egerváry theorem.

Setting

Fix two fields $K \subseteq F$ : typically $K = \mathbb{Q}$ and $F$ a field large enough to hold every number in the problem. A family $t_1, \dots, t_m \in F$ is algebraically independent over $K$ if no nonzero polynomial with coefficients in $K$ vanishes at $(t_1, \dots, t_m)$ — informally, the $t_i$ behave as free, unconstrained parameters relative to $K$ . Fix finite row and column index sets $R$ and $C$ . A matrix $A = (A_{ij})_{i \in R, j \in C}$ over $F$ is a mixed matrix with respect to $(K, F)$ if it decomposes as

A = Q + T

where $Q = (Q_{ij})$ has every entry in $K$ , and $T = (T_{ij})$ has entries in $F$ whose nonzero values, taken together as one family, are algebraically independent over $K$ . $Q$ models the exact, structural part of the system; $T$ models the independent physical parameters. For $I \subseteq R$ and $J \subseteq C$ , write $A[I,J]$ for the submatrix with rows $I$ and columns $J$ . The rank of $A$ is its rank over $F$ — equivalently, the size of the largest nonvanishing-determinant square submatrix. Write $\rho(I,J) = \operatorname{rank} Q[I,J]$ , $\tau(I,J) = \operatorname{rank} T[I,J]$ , and $\gamma(I,J)$ for the number of rows of $I$ that contain a nonzero entry of $T$ in some column of $J$ . A mixed polynomial matrix $A(s) = Q(s) + T(s)$ is the same decomposition applied entrywise to matrices whose entries are polynomials in an indeterminate $s$ (used to model the Laplace- or $z$ -transform variable of a linear time-invariant system): $Q(s)$ has every coefficient of every entry in $K$ , and the coefficients of $T(s)$ 's entries, taken together, are algebraically independent over $K$ .

Formalization targets

\textbf{Theorem 12.9 (goal).}\quad \text{For a mixed matrix } A=Q+T,\ \exists\, I \subseteq R,\ J \subseteq C:\quad |I|+|J|-\operatorname{rank} Q[I,J] = |R|+|C|-\operatorname{rank} A \ \ \text{and}\ \ \operatorname{rank} T[I,J] = 0.

This is the König–Egerváry theorem for mixed matrices: a combinatorial certificate of $A$ 's rank deficiency, generalizing the classical theorem relating the maximum matching size of a bipartite graph (equivalently, the rank of a 0-1 matrix) to a minimum vertex cover. It is reached via three supporting results, each a genuine theorem in its own right: Proposition 12.6 (nonsingularity of $A$ reduces to nonsingularity of a $Q$ -part and a $T$ -part on complementary index splits), Theorem 12.7 (the resulting rank max-formula), and Theorem 12.8 (the three dual min-formulas Theorem 12.9 is extracted from). Theorem 12.13 extends the max-formula to the degree of the determinant of a mixed polynomial matrix.

Significance

The result itself. Theorem 12.9 gives a certificate, not just a number: a pair $(I,J)$ that simultaneously proves the exact numeric rank contribution of $Q$ and exhibits a submatrix of $T$ that vanishes identically. Because $\rho$ (via Gaussian elimination on $Q$ ) and $\gamma$ , $\tau$ (via maximum bipartite matching on $T$ 's nonzero pattern) are each individually cheap to evaluate, and the min-max structure of Theorem 12.8 is exactly the kind of problem Edmonds's matroid intersection theorem (a special case of this book's Theorem 4.18) and this book's discrete convexity machinery solve efficiently, the whole rank computation for a mixed matrix — and hence the generic solvability test for a physical system modeled by one — is polynomial-time, despite Theorem 12.7's formula naively ranging over exponentially many index-set pairs.

Formalizing it. All five results in this mission are proved in the source text (this is textbook, not open, mathematics). What formalization adds is a machine-checked confirmation that the genericity hypothesis — "the nonzero entries of $T$ are algebraically independent" — is precisely what the printed proofs use, expressed through Mathlib's own AlgebraicIndependent rather than an informal paraphrase such as "generic" or "random" values, which would be either meaningless or a different (probabilistic) condition.

Difficulty

The naive approach to testing whether $A = Q+T$ is nonsingular is to expand $\det A$ directly and check whether the resulting expression, as a polynomial in $T$ 's free parameters, is the zero polynomial. This is exactly what genericity is supposed to let you avoid: Proposition 12.6's proof observes that the Laplace-type expansion $\det A = \sum_{|I|=|J|} \pm \det Q[I,J] \cdot \det T[R\setminus I, C\setminus J]$ has no cancellation between distinct terms, precisely because the nonzero entries of $T$ are algebraically independent — a coincidental cancellation would be a nontrivial polynomial relation among free parameters, which cannot happen. This turns a determinant computation with symbolic entries into a purely combinatorial search over row/column splits, each of whose two pieces is checked in the "easy" arithmetic appropriate to it (numeric determinant for $Q$ , a nonzero-pattern-only matching argument for $T$ ). Missing this point — e.g. by treating $T$ 's entries as merely "distinct" or "typically nonzero" rather than algebraically independent — reintroduces exactly the cancellation risk the theorem is built to rule out.

Formalization scope

Row and column index sets $R$ , $C$ are general finite types (Fintype, with DecidableEq where needed for Finset operations), not fixed to $\mathrm{Fin}\ n$ . No constant appears in any statement in this mission — every quantity (ranks, cardinalities, $\gamma$ ) is instance-dependent, so rule 7's explicit-constant obligation does not apply here. "Nonsingular" for a (possibly rectangular, cross-type-indexed) submatrix $M[I,J]$ is formalized as I.card = J.card together with rank M[I,J] = I.card (full rank) rather than via Matrix.det, because Mathlib's determinant requires both index sets to be the same Lean type, which I : Finset R and J : Finset C are not in general even when equinumerous; this coincides with ordinary nonsingularity whenever the ambient matrix is genuinely square. The degree of the determinant of a submatrix in Theorem 12.13 is computed the same way, via an arbitrary reindexing bijection between the row- and column-index subtypes — a choice that changes the determinant by at most a sign and hence never changes its degree. A formalization that replaced the genericity hypothesis on $T$ with mere distinctness of its nonzero entries would admit spurious cancellations in the determinant expansion and would not prove Proposition 12.6 or any of its consequences; AlgebraicIndependent K is the precise, non-trivializing condition the book's proofs use. This chapter is self-contained: no definitions from any other mission in this series are imported. Reusable beyond this mission: MatrixSubRank, IsNonsingularSub, and SubDegDet apply to any pair of matrices over any field, not only to mixed-matrix decompositions.

Selected references

Murota, K. Discrete Convex Analysis. SIAM, 2003. DOI: 10.1137/1.9780898718508. (Chapter 12.)
Murota, K. Matrices and Matroids for Systems Analysis. Springer, 2000.
Murota, K. "Systems Analysis by Graphs and Matroids: Structural Solvability and Controllability." Springer, 1987.
König, D. "Gráfok és mátrixok" (Graphs and matrices). Matematikai és Fizikai Lapok 38, 1931, 116–119.
Egerváry, J. "Matrixok kombinatorius tulajdonságairól" (On combinatorial properties of matrices). Matematikai és Fizikai Lapok 38, 1931, 16–28.

11 thms1 active userReviewed

Graph Theory·Captain: mikedeng1

Correspondence Coloring and Its Application to List-Coloring Planar Graphs Without Cycles of Lengths 4 to 8: Every Planar Graph Without Cycles of Lengths 4 to 8 Is 3-ChoosableResearch Paper

Motivation

List colouring asks for a proper colouring of a graph in which every vertex takes its colour from its own prescribed list. A graph is $k$ -choosable if such a colouring exists for every assignment of lists of size $k$ . Choosability is harder to guarantee than colourability: planar triangle-free graphs are 3-colourable (Grötzsch) but not all are 3-choosable (Voigt, 1995), and planar graphs are 4-colourable but not all 4-choosable (Voigt, 1993), while every planar graph is 5-choosable (Thomassen, 1994).

A long line of work asks which forbidden cycle lengths make a planar graph 3-colourable or 3-choosable, motivated by Steinberg's conjecture (every planar graph without cycles of lengths 4 and 5 is 3-colourable), which was disproved by Cohen-Addad, Hebdige, Král', Li and Salgado (arXiv:1604.05108).

Timeline.

1993–1995: Voigt constructs planar graphs that are not 4-choosable, and planar triangle-free graphs that are not 3-choosable.
1994: Thomassen proves that every planar graph is 5-choosable; in 1995 he proves that planar graphs of girth at least 5 (no cycles of lengths 3 and 4) are 3-choosable.
1996: Borodin proves that planar graphs without cycles of lengths 4 to 9 are 3-colourable; the proof also gives 3-choosability.
2005: Borodin, Glebov, Raspaud and Salavatipour prove 3-colourability when cycles of lengths 4 to 7 are forbidden.
2007: Voigt constructs a planar graph without cycles of lengths 4 and 5 that is not 3-choosable, so the list version of Steinberg's conjecture fails.
2013: Borodin's survey records as open, for more than fifteen years, whether excluding cycles of lengths 4 to 8 suffices for 3-choosability.
2018: Dvořák and Postle (arXiv:1508.03437, J. Combin. Theory Ser. B) answer the question positively. To do so they introduce correspondence colouring, now usually called DP-colouring, which has since become a standard tool.

Setting

All graphs are finite and simple. A list assignment $L$ gives each vertex $v$ a finite set $L(v)$ of colours; an $L$ -coloring is a map $\varphi$ with $\varphi(v)\in L(v)$ for all $v$ and $\varphi(u)\ne\varphi(v)$ on every edge $uv$ . $G$ is $k$ -choosable if an $L$ -coloring exists whenever $|L(v)|=k$ for all $v$ .

Write $[k]$ for a set of $k$ colours. A $k$ -correspondence assignment $C$ assigns to each edge $uv$ a partial matching $C_{uv}$ between $\{u\}\times[k]$ and $\{v\}\times[k]$ . A $C$ -coloring is a map $\varphi:V(G)\to[k]$ such that $(u,\varphi(u))$ and $(v,\varphi(v))$ are not matched in $C_{uv}$ for any edge $uv$ . Ordinary colouring is the case where every $C_{uv}$ matches equal colours.

For a closed walk $W=v_0v_1\dots v_m$ ( $v_m=v_0$ ), $C$ is inconsistent on $W$ if there are colours $c_0,\dots,c_m$ with $(v_i,c_i)(v_{i+1},c_{i+1})\in E(C_{v_iv_{i+1}})$ for every $i<m$ and $c_0\ne c_m$ ; otherwise it is consistent on $W$ . $C$ is consistent if it is consistent on every closed walk. An edge $uv$ is straight if $C_{uv}$ only matches equal colours, and full if $C_{uv}$ is a perfect matching.

A plane graph is a graph with a fixed drawing in the plane without crossings; its faces are the connected components of the complement of the drawing, and a vertex is incident with a face if it lies in the face's closure. A graph is planar if it has such a drawing.

Formalization targets

Goal: Theorem 1 (p. 3)

\text{Every planar graph } G \text{ without cycles of lengths } 4 \text{ to } 8 \text{ is } 3\text{-choosable.}

Milestones

Lemma 5 (p. 6): $G$ is $k$ -choosable iff $G$ is $C$ -colorable for every consistent $k$ -correspondence assignment $C$ .
Lemma 7 (p. 10): if every cycle of a subgraph $H$ has full edges and $C$ is consistent on it, then renaming colours at the vertices of $H$ makes every edge of $H$ straight.
Lemmas 10, 11, 12 (pp. 14–16): properties of a minimal counterexample to Theorem 8 — dense matchings, full triangles next to degree-three vertices, and every tetrad (a path of four degree-three vertices on a face whose end edges lie in triangles) meets the precoloured set.
Theorem 8 (p. 11): for a plane graph $G$ without cycles of lengths 4 to 8, a set $S$ with $|S|\le 1$ or $S$ = all vertices of one face, $|S|\le 12$ , and a 3-correspondence assignment $C$ consistent on closed walks of length 3, every $C$ -coloring of $G[S]$ extends to a $C$ -coloring of $G$ .
Theorem 6 (p. 7): every planar graph without cycles of lengths 4 to 8 is $C$ -colorable for every 3-correspondence assignment $C$ consistent on every closed walk of length 3.

Theorem 8 implies Theorem 6 ( $S=\emptyset$ ), and Theorem 6 with Lemma 5 implies Theorem 1.

Significance

The result. Theorem 1 settles Borodin's question and is still the best known forbidden-interval result for 3-choosability of planar graphs with triangles allowed. Theorem 6 is a strengthening in the correspondence setting, and Theorem 8, a precolouring-extension statement, is the form used for induction. The broader contribution is correspondence colouring itself: it allows reductions that identify vertices, which list colouring does not, and it has since been developed by Bernshteyn, Kostochka, Pron and many others as DP-colouring.

Formalizing it. The results are proved in the paper; none has a machine-checked proof. Mathlib has no planarity, no list colouring and no correspondence colouring. This mission produces the first formal definitions of $k$ -choosability and correspondence colouring on the platform, the equivalence between list colouring and consistent correspondence colouring (Lemma 5), and a formal statement of the planar result, together with the paper's reduction lemmas as independent targets.

Difficulty

Lemma 5 and Lemma 7 are finite combinatorics. The main obstacle is Theorem 8. The natural list-colouring argument by reducible configurations fails: reductions for ordinary colouring identify two vertices, which is meaningless when their lists differ. Correspondence colouring removes that obstruction only when the identification does not create parallel edges or short cycles, and the main reduction (Lemma 12) needs consistency on triangles, which is why Theorem 6 carries that hypothesis. On the formal side, the proof uses planar topology: faces, the open disk bounded by a cycle, 2-connectedness of a minimal counterexample, and a discharging argument over faces that relies on Euler's formula. None of this exists in Mathlib.

Formalization scope

Conventions committed to in the Lean statements:

Graphs are SimpleGraph V on a Fintype vertex type; the paper's graphs are finite and simple (p. 3).
$k$ -choosability quantifies over an arbitrary colour type α : Type and lists L : V → Finset α of cardinality exactly $k$ .
A $k$ -correspondence assignment is a relation M u c v d on V × Fin k × V × Fin k that lives on edges, is symmetric, and is a partial matching. The paper's $[k]=\{1,\dots,k\}$ is Fin k.
Consistency is defined on Mathlib closed walks G.Walk v v through getVert. The paper's example of Figure 1(a) (p. 5) was checked against this definition by a sorry-free local proof.
Planarity and plane graphs use straight-line drawings in ℝ × ℝ: injective vertex positions, no vertex on a non-incident edge, and disjoint segments for edges with no common end. These are the clauses of the platform's OPG401.IsPlanar. By Fáry's theorem this is equivalent to planarity for finite simple graphs, and every plane graph has a straight-line drawing with the same faces. Faces are components of the complement of the drawing, incidence is membership in the closure, and the outer face is the unbounded face. Theorem 8 is stated for every drawing and any face, not only the outer one.
"Renaming on vertices of $X$ " between two 3-correspondence assignments is a permutation of $[k]$ at each vertex of $X$ , the identity elsewhere. This is exactly the effect of the paper's sequences of single renamings.
A target (p. 11) has its vertex type in Type. The measure $s(B)$ counts ordered pairs, which gives the same lexicographic order. A minimal counterexample is minimal among all targets of this kind.

Formalizations that would trivialize or change the problem are ruled out:

a girth bound, which excludes triangles;
lists drawn from a fixed 3-element palette (3-colourability);
a planarity surrogate such as an edge bound;
a correspondence that is not a matching;
consistency without the closing condition $c_0\ne c_m$ ;
consistency on all closed walks in Theorems 6 and 8.

Infrastructure needed and reusable beyond this mission: planar straight-line drawings and their faces (Euler's formula, the Jordan curve theorem for polygons), 2-connectivity and facial cycles, and a DP-colouring library (renaming, consistency, Lemma 5). Contributions to any of these are welcome. So are proofs of Lemma 5 and Lemma 7, which need no topology.

Selected references

Z. Dvořák, L. Postle, Correspondence coloring and its application to list-coloring planar graphs without cycles of lengths 4 to 8, J. Combin. Theory Ser. B (2018); cited version arXiv:1508.03437v2 (2016). https://arxiv.org/abs/1508.03437
O. V. Borodin, Colorings of plane graphs: a survey, Discrete Math. 313 (2013) 517–539.
O. V. Borodin, Structural properties of plane graphs without adjacent triangles and an application to 3-colorings, J. Graph Theory 21 (1996) 183–186.
O. V. Borodin, A. N. Glebov, A. Raspaud, M. R. Salavatipour, Planar graphs without cycles of length from 4 to 7 are 3-colorable, J. Combin. Theory Ser. B 93 (2005) 303–311.
V. Cohen-Addad, M. Hebdige, D. Král', Z. Li, E. Salgado, Steinberg's conjecture is false, J. Combin. Theory Ser. B (2017). https://arxiv.org/abs/1604.05108
C. Thomassen, Every planar graph is 5-choosable, J. Combin. Theory Ser. B 62 (1994) 180–181.
C. Thomassen, 3-list-coloring planar graphs of girth 5, J. Combin. Theory Ser. B 64 (1995) 101–107.
M. Voigt, List colourings of planar graphs, Discrete Math. 120 (1993) 215–219.
M. Voigt, A not 3-choosable planar graph without 3-cycles, Discrete Math. 146 (1995) 325–328.
M. Voigt, A non-3-choosable planar graph without cycles of length 4 and 5, Discrete Math. 307 (2007) 1013–1015.

16 thms1 active userReviewed

Probability·Captain: mikedeng1

Limits of Permutation Sequences II: Convergence Is Equivalent to Being Cauchy in the Rectangular DistanceResearch Paper

Motivation

For dense graphs, convergence of subgraph densities was shown by Lovász and Szegedy (2006) to have graphons as limit objects, and Borgs, Chayes, Lovász, Sós and Vesztergombi (2008) proved that the same convergence is metric: a graph sequence converges exactly when it is Cauchy in the cut distance. The metric view is what makes the space of graphons compact and connects limit theory with regularity lemmas and property testing.

Hoppen, Kohayakawa, Moreira, Ráth and Sampaio (arXiv:1103.5844; J. Combin. Theory Ser. B, 2013) developed the corresponding theory for permutations. Besides the existence of limits (the subject of mission I of this series), they introduced a rectangular distance $d_\square$ between permutations, a normalized version of Cooper's discrepancy (Cooper, J. Combin. Theory Ser. A, 2004; reference [7] of the paper), and proved in Theorem 1.8 that convergence of a permutation sequence is the same as being Cauchy for $d_\square$ . This mission formalizes that theorem.

Timeline:

2004. Cooper introduces the discrepancy of a permutation as a measure of quasirandomness.
2006–2008. Lovász–Szegedy and Borgs et al. establish graph limits and the cut-distance characterization of convergence.
2011–2013. Hoppen et al. prove the permutation analogues, including Theorem 1.8 (this paper).

Setting

For $n \ge 1$ , $S_n$ is the set of permutations of $[n]=\{1,\dots,n\}$ , $|\pi| = n$ for $\pi\in S_n$ , and $\mathcal S=\bigcup_n S_n$ . For $\tau\in S_k$ and $\pi\in S_n$ , $\Lambda(\tau,\pi)$ counts the increasing $k$ -tuples $x_1<\dots<x_k$ in $[n]$ with $\pi(x_i)<\pi(x_j)\iff\tau(i)<\tau(j)$ , and the subpermutation density is $t(\tau,\pi)=\Lambda(\tau,\pi)/\binom nk$ for $k\le n$ and $0$ for $k>n$ . A permutation sequence $(\sigma_n)$ is convergent if $t(\tau,\sigma_n)$ converges for every fixed $\tau\in\mathcal S$ .

A limit permutation is a Lebesgue measurable $Z:[0,1]^2\to[0,1]$ such that $Z(x,\cdot)$ is a cdf (non-decreasing, right-continuous, $Z(x,1)=1$ ) for every $x$ and $\int_0^1 Z(x,y)\,dx=y$ for every $y$ ; the set of them is $\mathcal Z$ . Each $Z$ has an associated random point $(X,Y)$ with $X\sim U[0,1]$ and conditional cdf $Z(X,\cdot)$ , joint distribution function $F(x,y)=\int_0^x Z(t,y)\,dt$ , and pattern densities $t(\tau,Z)$ (the probability that $k$ independent copies of $(X,Y)$ form the pattern $\tau$ ).

For $\sigma\in S_n$ , the step limit permutation $Z_\sigma$ spreads the permutation matrix of $\sigma$ uniformly over the corresponding $n\times n$ grid cells. The rectangular distance of $Z_1,Z_2\in\mathcal Z$ is

d_\square(Z_1,Z_2)=\sup_{x_1<x_2,\ y_1<y_2}\left|\int_{x_1}^{x_2}\big(Z_1(x,y_2)-Z_1(x,y_1)\big)dx-\int_{x_1}^{x_2}\big(Z_2(x,y_2)-Z_2(x,y_1)\big)dx\right|,

the largest difference between the probabilities the two random points give to an axis-parallel rectangle, and $d_\infty(Z_1,Z_2)=\sup_{x,y}|F_1(x,y)-F_2(x,y)|$ . On permutations of possibly different lengths, $d_\square(\sigma,\pi):=d_\square(Z_\sigma,Z_\pi)$ . A sequence is Cauchy with respect to $d_\square$ if for every $\varepsilon>0$ there is $n_0$ with $d_\square(\sigma_n,\sigma_m)<\varepsilon$ for all $n,m\ge n_0$ .

Formalization targets

Goal: Theorem 1.8, under $|\sigma_n|\to\infty$

|\sigma_n|\to\infty\ \Longrightarrow\ \Big((\sigma_n)\ \text{convergent}\iff(\sigma_n)\ \text{is } d_\square\text{-Cauchy}\Big).

Milestones

In the order the proof uses them:

Lemma 3.5: $|t(\tau,\sigma)-t(\tau,Z_\sigma)|\le\frac1n\binom k2$ for $\tau\in S_k$ , $\sigma\in S_n$ , $k\le n$ .
Eq. (49): for $|\sigma_n|\to\infty$ , $\sigma_n\to Z\iff Z_{\sigma_n}\xrightarrow{t}Z$ .
Eq. (34): $d_\infty\le d_\square\le 4\,d_\infty$ on $\mathcal Z$ .
Lemma 2.1: for uniform marginals, weak convergence is equivalent to uniform convergence of joint distribution functions.
Lemma 2.2 (a): every law on $[0,1]^2$ with uniform marginals has a limit permutation as its conditional cdf.
Lemma 5.3: weak, $d_\square$ - and density convergence on $\mathcal Z$ coincide.
Theorem 1.6 (i): a convergent sequence with $|\sigma_n|\to\infty$ converges to some $Z\in\mathcal Z$ .
Claim 2.4: a convergent sequence with $|\sigma_n|\not\to\infty$ is eventually constant.
Theorem 1.8 ( $\Rightarrow$ ): every convergent sequence is $d_\square$ -Cauchy, with no condition on lengths.

Significance

Theorem 1.8 identifies density convergence, defined through infinitely many pattern counts, with a single metric condition. With Theorem 1.6 it shows that the completion of $(\mathcal S,d_\square)$ is $\mathcal Z$ modulo almost-everywhere equality, which is compact; permutations are isolated points of it (Claim 2.4). This is the permutation counterpart of the cut-distance theory of graph limits, and it is the metric in which the paper's testability and sampling results (Lemma 4.2) are quantitative.

The theorem is proved in the paper. To the best of current knowledge neither it nor the underlying permuton theory is formalized in any proof assistant. The mission produces machine-checked statements of the rectangular distance, its comparison with the sup-norm distance of distribution functions, and the Cauchy characterization, all reusable for quasirandom permutations and permutation property testing.

Difficulty

The direction "convergent $\Rightarrow$ Cauchy" needs a limit permutation for the sequence and the equivalence of density and $d_\square$ convergence on $\mathcal Z$ (Lemma 5.3), which is not formal: density convergence involves every pattern, $d_\square$ a supremum over rectangles. For "Cauchy $\Rightarrow$ convergent", completeness of bounded functions under the sup norm gives a uniform limit $F$ of the distribution functions, but a uniform limit of distribution functions of limit permutations is not visibly the distribution function of a limit permutation. Identifying it needs weak compactness, Lemma 2.1 and the regular conditional cdf of Lemma 2.2.

The literal statement also fails for sequences whose lengths do not tend to infinity, as explained under Formalization scope; the reduction "we may assume $|\sigma_n|\to\infty$ " covers only one direction.

Formalization scope

$[0,1]$ is Mathlib's unitInterval with Lebesgue measure; a limit permutation is a curried real function Z : I → I → ℝ, almost-everywhere measurable on the square, with the cdf and integral conditions for every $x$ and every $y$ . $S_n$ is Equiv.Perm (Fin n) (0-based) and a permutation sequence is ℕ → Σ n, Equiv.Perm (Fin n).
$d_\square$ on $\mathcal Z$ is the integral form of the paper's Eq. (32); $d_\infty$ is Eq. (33) with $F_i(x,y)=\int_0^x Z_i(t,y)\,dt$ . Both are real suprema of bounded families. $Z_\sigma$ is in closed form, with the first row used at $x=0$ (a null-set choice).
$d_\square$ on permutations is defined for every pair of lengths as $d_\square(Z_\sigma,Z_\pi)$ , the paper's extension (Sect. 4.1); the same-length formula (31) is not needed. A definition that returned $0$ or junk for different lengths would make every sequence with growing lengths Cauchy and is ruled out.
Correction. The paper states Theorem 1.8 for all sequences. Without $|\sigma_n|\to\infty$ , "Cauchy $\Rightarrow$ convergent" is false: interleaving $\sigma=(1,2)$ with permutations $\tau_k$ , $|\tau_k|\to\infty$ , $d_\square(Z_{\tau_k},Z_\sigma)\to0$ , gives a Cauchy sequence along which $t(\sigma,\cdot)$ alternates between $1$ and values tending to $3/4$ . The goal carries $|\sigma_n|\to\infty$ ; the true direction without it is milestone 9.
"Convergent" is the paper's Definition 1.2 (all densities converge), not the existence of a limit $Z$ . The Cauchy condition uses the explicit $\varepsilon$ – $n_0$ form with strict inequality, not a metric-space instance.
Theorem 1.6 (i) is also the goal of mission I; it is restated here in this mission's namespace.

Needed infrastructure: Prokhorov compactness of probability measures on the square, the Portmanteau theorem, completeness of bounded functions under the sup norm, and conditional cdfs (ProbabilityTheory.condCDF). Contributions on any milestone, and alternative proofs of the Cauchy characterization, are welcome.

Selected references

C. Hoppen, Y. Kohayakawa, C. G. Moreira, B. Ráth, R. M. Sampaio, Limits of permutation sequences, arXiv:1103.5844v2, 2012; J. Combin. Theory Ser. B 103 (2013). https://arxiv.org/abs/1103.5844v2
J. N. Cooper, Quasirandom permutations, J. Combin. Theory Ser. A 106 (2004) no. 1, 123–143 (cited as [7] in arXiv:1103.5844v2).
L. Lovász, B. Szegedy, Limits of dense graph sequences, J. Combin. Theory Ser. B 96 (2006) 933–957. https://doi.org/10.1016/j.jctb.2006.05.002
C. Borgs, J. T. Chayes, L. Lovász, V. T. Sós, K. Vesztergombi, Convergent sequences of dense graphs I: Subgraph frequencies, metric properties and testing, Adv. Math. 219 (2008) 1801–1851. https://doi.org/10.1016/j.aim.2007.08.004
P. Billingsley, Convergence of Probability Measures, 2nd ed., Wiley, 1999. https://doi.org/10.1002/9780470316962

19 thms1 active userReviewed

Graph Theory Operations Research·Captain: mikedeng1

Graph Minors. V. Excluding a Planar Graph: Bounded Tree-Width without a Planar MinorResearch Paper

Motivation

Tree-width measures how closely a graph resembles a tree. Graphs of bounded tree-width admit dynamic-programming algorithms for problems that are NP-hard in general (colouring, Hamiltonicity, and every property expressible in monadic second-order logic, by Courcelle's theorem), which is why the parameter is central to parameterized complexity and to combinatorial optimization on sparse networks. The question this mission addresses is structural: which excluded substructures force bounded tree-width?

The answer is the Excluded Grid Theorem of Robertson and Seymour: excluding a fixed graph $H$ as a minor bounds the tree-width if and only if $H$ is planar. The "only if" direction is easy, since grids are planar and have unbounded tree-width. The "if" direction is the content of Graph Minors. V. Excluding a Planar Graph (J. Combin. Theory Ser. B 41 (1986) 92–114). It is a cornerstone of the Graph Minors series that culminates in the Robertson–Seymour theorem (graphs are well-quasi-ordered by the minor relation), and it underlies polynomial-time minor testing for planar $H$ (Graph Minors XIII) and the Erdős–Pósa-type results of Sect. 8 of the same paper.

Timeline. Robertson and Seymour, Graph Minors V (1986): tree-width at most an explicit, iterated-exponential function of the grid size. Robertson, Seymour and Thomas, Quickly excluding a planar graph (JCTB 62, 1994): bound $2^{O(\theta^5)}$ for the $\theta$ -grid. Chekuri and Chuzhoy (J. ACM 2016): the first polynomial bound. Chuzhoy and Tan (JCTB 2021): $O(\theta^9\,\mathrm{polylog}\,\theta)$ .

Setting

Graphs are finite. A graph $H$ is a minor of $G$ if $H$ can be obtained by contraction from a subgraph of $G$ ; equivalently, there are nonempty, pairwise disjoint vertex sets $\beta(w)\subseteq V(G)$ , one per vertex $w$ of $H$ , each inducing a connected subgraph, such that every edge $ab$ of $H$ is matched by an edge of $G$ between $\beta(a)$ and $\beta(b)$ .

A tree-decomposition of $G$ is a tree $T$ together with bags $X_t\subseteq V(G)$ ( $t\in V(T)$ ) such that every vertex lies in some bag, both ends of every edge lie in a common bag, and $X_t\cap X_{t''}\subseteq X_{t'}$ whenever $t'$ lies on the path of $T$ between $t$ and $t''$ . Its width is $\max_t(|X_t|-1)$ , and the tree-width $\mathrm{tw}(G)$ is the least width of a tree-decomposition of $G$ .

The $\theta$ -grid has vertex set $\{v_{ij}: 1\le i,j\le\theta\}$ , with $v_{ij}$ adjacent to $v_{i'j'}$ exactly when $|i-i'|+|j-j'|=1$ . For even $\theta\ge 6$ , $\mathcal F_\theta$ is the class of graphs with no minor isomorphic to the $\theta$ -grid. Every planar graph $H$ is a minor of some even grid of size at least 6; $\theta(H)$ denotes the least such size.

The paper fixes explicit parameters. For $k\ge 2$ : $\alpha(2,n)=n+1$ and $\alpha(k,n)=2^{n\theta^4}+\alpha(k-1,2^{n\theta^4}+n+1)$ . Then $\theta_1=2\alpha(\theta^2/2,\theta^2/2)$ ; $\phi_{\theta_1}=\theta^2/2$ and $\phi_k=\phi_{k+1}2^{\phi_{k+1}\theta^2}$ ; $\theta_2=\phi_0+2\phi_1+\dots+2\phi_{\theta_1-1}+\phi_{\theta_1}$ ; $\theta_3=(\theta^2/2)^{\theta_2-1}$ ; $\theta_4=\theta_2\binom{\theta_3}{\theta_2}+\tfrac12\theta^2\binom{\theta_3}{\theta^2/2}$ ; $\theta_5=(\theta^2/2)^{\theta_4-1}$ ; $\theta_6=\theta_3\binom{\theta_5}{\theta_4}+\tfrac12\theta^2\binom{\theta_5}{\theta^2/2}$ ; $\theta_7=\alpha(\theta_5,\theta_6)$ ; $\theta_8=3\theta_5(3^{\theta_5}-1)/4$ ; $\theta_9=\theta_7(\theta_8+1)+1$ .

Two auxiliary structures carry the argument. An $(m,n)$ -web is a pair of families of paths $(A_1,\dots,A_m)$ , $(B_1,\dots,B_n)$ , each family vertex-disjoint, every $A_i$ meeting every $B_j$ , and all $m+n$ paths pairwise edge-disjoint. An $(m,n)$ -mesh is the same with arbitrary connected subgraphs in place of paths and without edge-disjointness.

Formalization targets

Goal: (2.1)

For every finite planar graph $H$ and every finite graph $G$ ,

H \not\preceq G \;\Longrightarrow\; \mathrm{tw}(G)\le\theta_9\bigl(\theta(H)\bigr).

Principal theorem: (7.3)

For even $\theta\ge 6$ and $G\in\mathcal F_\theta$ ,

\mathrm{tw}(G)\le\theta_9.

Intermediate targets

Sect. 2: every planar graph is a minor of some even $\theta$ -grid, $\theta\ge 6$ .
(3.2): $n$ disjoint connected subgraphs meeting each of $V_1,\dots,V_k$ , or a hitting set of size $<\alpha(k,n)$ .
(4.1), (4.2), (4.4), (4.5), (4.6): no $(\theta_2,\theta_2)$ -web in $G\in\mathcal F_\theta$ .
(5.1), (5.2), (5.3): no $(\theta_5,\theta_6)$ -mesh in $G\in\mathcal F_\theta$ .
(6.2), (6.3), (6.4): weighted and unweighted balanced-cut lemmas valid for all graphs.
(7.1), (7.2): separations of order $\le\theta_7$ splitting $V(G)$ , or any $X\subseteq V(G)$ , in ratio $1-\theta_8^{-1}$ .

Significance

The theorem converts a qualitative exclusion (no $H$ minor) into a quantitative width bound, and it is the entry point of the structure theory of minor-closed classes: every minor-closed class excluding a planar graph has bounded tree-width, and hence all MSO-definable problems on it are solvable in linear time. It is used in the proof of the graph minor theorem, in minor testing, and in the Erdős–Pósa property for planar minors (Sect. 8 of the paper).

The result is proved and classical; to our knowledge it has not been machine-checked in any proof assistant, and Mathlib has no graph minors, tree-decompositions or Menger's theorem. A formalization produces reusable definitions (branch-set minors, tree-decompositions, separations, grids) and a checked proof of the paper's explicit bound. The goal is stated with the paper's constant $\theta_9$ , not an optimized one; later improvements are stronger variants, not replacements.

Difficulty

The obvious attempt, building a tree-decomposition greedily from small separations, fails because nothing forces small balanced separations to exist. The whole argument supplies them: a graph without a large grid minor has no large mesh (5.3), and a graph with no large mesh has a balanced separation of bounded order (7.1). The step from no grid to no mesh goes through webs and spiders (Sect. 4) and relies on two results from Graph Minors I ((3.1) and (4.3) of the paper, cited without proof), which themselves depend on Menger's theorem. The balanced-cut lemmas (6.2)–(6.4) rest on Tutte's ordering of 2-connected graphs. None of this infrastructure exists in Mathlib.

Formalization scope

Graphs are Mathlib SimpleGraphs on finite types (Fintype V, DecidableEq V). The paper allows loops and multiple edges; for $G$ this changes nothing, since every notion used depends only on adjacency, and for $H$ in the goal it specializes the theorem to simple planar graphs. Minors use the branch-set model (IsMinor); planarity (IsPlanar) is the existence of a crossing-free drawing in $\mathbb R^2$ , mirroring the platform's FourColor.IsPlanar. Tree-width is not defined as an infimum; "tree-width at most $w$ " (TreewidthLE) is the existence of a tree-decomposition with all bags of size $\le w+1$ over a finite tree. $\theta(H)$ enters the goal as a hypothesis IsLeast {t | Even t ∧ 6 ≤ t ∧ IsMinor H (grid t)} θ, which is satisfiable for every planar $H$ by the Sect. 2 milestone, so the goal is not vacuous. Every statement of Sects. 3–7 that mentions $\theta$ carries the standing assumption " $\theta$ even, $\theta\ge 6$ " as hypotheses. Rational bounds such as $(1-\theta_8^{-1})|V(G)|$ and $2(3^k-1)^{-1}|V(G)|$ are compared in $\mathbb Q$ .

Two printed statements are corrected. (4.5) is printed for $0\le k<\theta_2$ and is stated for $0\le k<\theta_1$ , the only range on which $\phi_{k+1},\psi_{k+1}$ are defined. (5.1) is false as printed for $p=1$ , $q\ge 1$ , so it carries the hypothesis " $p=1$ implies $q=0$ "; the paper uses it only with $p=\theta^2/2$ .

Needed infrastructure, reusable well beyond this mission: Menger's theorem, the Graph Minors I linkage results, Tutte's ordering of 2-connected graphs, and a library of lemmas for minors and tree-decompositions. Proofs of any milestone, of the cited results as separate theorems, and of basic API for the definitions are welcome.

Selected references

N. Robertson, P. D. Seymour, Graph Minors. V. Excluding a Planar Graph, J. Combin. Theory Ser. B 41 (1986) 92–114. https://doi.org/10.1016/0095-8956(86)90030-4
N. Robertson, P. D. Seymour, Graph Minors. I. Excluding a Forest, J. Combin. Theory Ser. B 35 (1983) 39–61. https://doi.org/10.1016/0095-8956(83)90079-5
N. Robertson, P. D. Seymour, R. Thomas, Quickly Excluding a Planar Graph, J. Combin. Theory Ser. B 62 (1994) 323–348. https://doi.org/10.1006/jctb.1994.1073
C. Chekuri, J. Chuzhoy, Polynomial Bounds for the Grid-Minor Theorem, J. ACM 63 (2016), Art. 40. https://doi.org/10.1145/2820609
J. Chuzhoy, Z. Tan, Towards Tight(er) Bounds for the Excluded Grid Theorem, J. Combin. Theory Ser. B 146 (2021) 219–265. https://doi.org/10.1016/j.jctb.2020.09.010
B. Courcelle, The Monadic Second-Order Logic of Graphs. I. Recognizable Sets of Finite Graphs, Information and Computation 85 (1990) 12–75. https://doi.org/10.1016/0890-5401(90)90043-H

28 thms1 active userReviewed

Discrete Geometry Graph Theory·Captain: aarontcao

Lovasz Problem 11.8: triangle-free unit vector systems sum to Theta(n^(2/3))Research Paper

Let $u_1, \dots, u_n$ be unit vectors in a Euclidean space such that among any three of them some two are orthogonal. How large can $\|u_1 + \dots + u_n\|$ be?

The answer is $\Theta(n^{2/3})$ .

Attribution, which is commonly given wrong in both halves

Lovasz posed the question, as Problem 11.8 of Combinatorial Problems and Exercises (North Holland, 1979). Konyagin proved the $O(n^{2/3})$ upper bound in Systems of vectors in Euclidean space and an extremal problem for polynomials, Mat. Zametki 29 (1981) 63-74, doi:10.1007/BF01142512. Alon gave a matching lower bound in Explicit Ramsey graphs and orthonormal labelings, Electron. J. Combin. 1 (1994) R12, doi:10.37236/1192. The two together pin the exponent exactly.

Where the proof comes from

The hypothesis is a graph condition in disguise. Join $i$ to $j$ when $\langle u_i, u_j \rangle \ne 0$ ; then "among any three some two are orthogonal" says that graph is triangle-free.

The proof does not run through Ramsey counting, which is the natural first guess and does not reach the right exponent. It runs through the Lovasz theta function. Kashin and Konyagin bound $\theta = O(n^{1/3})$ for graphs of independence number less than 3, that is for complements of triangle-free graphs, and Cauchy-Schwarz turns that into the bound on the norm of the sum. The orthonormal labeling of a graph by unit vectors is not a coincidence of notation: it is the definition of $\theta$ that the argument uses.

What this mission will cost

State this honestly rather than discover it later. The Lovasz theta function, orthonormal graph labeling, and Shannon capacity are all absent from Mathlib. So the milestone chain that the upper bound needs cannot be written yet, and this proposal ships with exactly one milestone, which is Alon's lower bound.

google-deepmind/formal-conjectures contains an SDP-form definition of the theta function, with basic bounds such as lovaszThetaFunction_le_card since PR #6100 of 2026-09-18. The proof here needs the orthonormal-labeling form instead, so that file is a starting point rather than a foundation. Building the theta function, proving that the two forms agree, and getting the Kashin-Konyagin bound is the real content of this mission and is larger than the statement of the goal suggests.

The lower bound is the tractable half. It needs explicit Ramsey graphs and an orthonormal labeling of one, and it does not need $\theta$ at all.

Notes on the formalization

Both items are stated in Mathlib primitives alone, so the mission omits definition items. The triangle-free hypothesis is written as a condition on triples of indices rather than through SimpleGraph.CliqueFree 3, so that a reader auditing the statement does not have to unfold a graph construction to see what is assumed. Anyone proving it is free to build the graph and use the Mathlib predicate.

2 thms1 active userReviewed

Graph Theory·Captain: Minghui

Formalize the Four Color Theorem in Lean 4Research Paper

Why formalize the Four Color Theorem in Lean 4?

The Four Color Theorem links a short mathematical statement to a large collection of finite checks. For contributors to graph theory and proof assistants, it is a concrete test of whether abstract mathematics, executable verification, and a public theorem statement can share one auditable foundation. The proposed result is a complete Lean 4 formalization, reusing Mathlib and adapting the established proof architecture to Lean.

The mathematical result is established. Robertson, Sanders, Seymour, and Thomas gave a modern computer-assisted proof in 1997. Gonthier subsequently developed a Coq formalization covering both mathematical reasoning and computation, described in his 2005 report and 2008 Notices article. This mission is classified as ResearchPaper because it formalizes these published results. (RSST, Gonthier 2005, Gonthier 2008)

Graphs, drawings, and colors

The root Lean interface uses Mathlib's SimpleGraph: a finite vertex set with a symmetric, irreflexive adjacency relation. Edges in this representation carry no additional identities or multiplicities. The conventional statement also permits parallel edges. Already-proved local infrastructure uses Mathlib's Graph V E to erase parallel edges while preserving a genuine plane drawing and proper vertex colorings; only the actual vertex set must be finite. A proper vertex coloring assigns a color to every vertex and assigns different colors to adjacent vertices. Four available colors means at most four colors are used; there is no requirement that each color occur.

A planar drawing places distinct vertices at distinct points of the real plane and represents each edge by an injective continuous arc joining its endpoints. An arc contains no other vertex, and arcs of different undirected edges meet only at shared endpoints. Reversing the orientation of an edge reverses its parameterization. A graph is planar when such a drawing exists. This is a geometric condition independent of coloring and of the eventual configuration checkers. Gonthier discusses the graph-embedding formulation in Section 2, PDF p. 4 of the 2005 report.

Write $V$ for the vertex set, $G$ for its adjacency relation, and $C=\{0,1,2,3\}$ for the available colors. Empty graphs, isolated vertices, and disconnected graphs are included. The drawing is a witness to a hypothesis; the theorem does not impose coordinates, a prescribed embedding, or a straight-line representation.

Formalization target

For every finite loopless planar graph, establish

\forall\,G=(V,E),\qquad \operatorname{Planar}(G)\Longrightarrow \exists c:V\to C,\quad \forall v,w\in V,\ \{v,w\}\in E\Longrightarrow c(v)\ne c(w).

The draft Lean target is FourColor.four_color: for every finite vertex type and every SimpleGraph on that type, FourColor.IsPlanar G implies G.Colorable 4. Its graph formulation follows RSST's Section 1, PDF p. 2 of the author-hosted manuscript. The manuscript's PDF page numbers differ from the journal's pagination.

The exact unchanged root signature is:

FourColor.four_color.{u} :
  ∀ (V : Type u) [Finite V] (G : SimpleGraph V),
    FourColor.IsPlanar G → G.Colorable 4

This is an open target signature, not a completed proof. The existing FourColor.FinalAudit.multigraph_four_color_of_necessary_targets conditionally connects the mission obligations to the conventional finite loopless planar multigraph statement. Its drawing has distinct vertex positions and injective continuous arcs for each edge identity; erasing parallel edges is proved to preserve planarity and every proper-coloring constraint. This bridge adds no simplicity, connectedness, triangulation, or nonemptiness assumption to the conventional conclusion. The root target itself remains unchanged.

An equivalent combinatorial formulation is welcome only with the formally verified translations needed to recover this target. If equivalence is claimed, both directions must be proved under precisely stated conventions. In particular, a hypermap coloring theorem alone does not complete this mission.

The original seven structural milestones remain unchanged:

Milestone	Deliverable
1. Graph realization	Construct a planar plain hypermap whose faces represent exactly the nonisolated graph vertices and whose edge steps encode precisely adjacency.
2. Cubic normalization	Construct a plain cubic hypermap with six times as many darts, preserving planarity and bridgelessness and transporting a coloring back.
3. Minimal counterexample	Choose a least-dart counterexample within the planar, bridgeless, plain, precubic comparison class.
4. Counterexample structure	Prove cubicity, connectedness and minimum face arity five as consequences of minimality.
5. Charge conservation	Prove total face charge $120c$ for $c$ components under arbitrary rational dart transfers, and a positive-charge face when connected.
6. Elimination	Complete the source's reducibility and unavoidability analysis to exclude every minimal counterexample.
7. Hypermap theorem	Assemble four-colorability for all planar bridgeless hypermaps.

These correspond to Gonthier's reductions in Section 3, PDF pp. 6–9, and development in Sections 5.1–5.6 of the 2005 report. Exact locations and executable-reference declarations accompany each milestone. Milestones 2, 3 and 6 imply milestone 7; milestones 1 and 7 imply the graph target. Those two conditional implications have been checked in Lean against the exact proposed statements. Milestone 6 now has thirteen concrete supporting targets:

Core target	Deliverable
Catalogue geometry	Prove geometric admissibility of every one of the fixed 633 configurations.
Catalogue reducibility	Kernel-check reducibility of every fixed map and contract using the proved complete checker or a verified refinement.
Reflection	Prove that the explicit mirror preserves minimal counterexamples.
Geometric exclusion	Prove that a C-reducible configuration cannot occur in a minimal counterexample; this includes the Birkhoff and patching arguments.
Presentation soundness	Prove the concrete finite presentation checker's generic soundness as one route to coverage.
Seven coverage cases	Independently handle positive hubs of degrees 5, 6, 7, 8, 9, 10 and 11, allowing reflected occurrences and unbounded neighboring arities.
Transfer bound	Bound each directed transfer by five under the explicit absence-of-configurations hypothesis; proved arithmetic then excludes positive hubs of degree at least 12.

The fixed catalogue and fixed rules are shared by both branches. The local Lean assembly checks that reducibility, geometric exclusion, reflection, the transfer bound, the seven degree cases, and milestones 4–5 imply milestone 6. It then connects to the unchanged hypermap and graph targets. The generic presentation checker offers a sufficient route to the semantic degree targets; its ability to certify every source presentation is not presumed. That route also requires actual presentation certificates and proofs of acceptance for the degree cases. Generic soundness and catalogue geometry alone do not supply those witnesses. Direct proofs of the seven semantic coverage obligations remain valid. Catalogue geometry remains a separate, meaningful finite theorem.

Exact mission obligations

There are 21 open theorem targets: 20 supporting milestones and one root. Every name below has prefix FourColor.. All remain future mission work; the checked conditional assembly is not a proof of any of these targets.

#	Exact target name	Obligation
1	`graph_realization`	Realize a finite drawn graph by a planar plain hypermap with exact face/adjacency incidence.
2	`cubic_normalization`	Construct the sixfold plain cubic map with the stated preservation and coloring transport.
3	`minimal_counterexample_exists`	Select a least-dart counterexample in the precubic comparison class.
4	`minimal_counterexample_structure`	Derive cubicity, connectedness and face arity at least five from minimality.
5	`charge_conservation`	Prove total charge and existence of a positive face for a connected host.
6	`catalogue_embeddable`	Prove the fixed 633 entries satisfy configuration geometry.
7	`catalogue_reducibility_certificates`	Establish accepted reducibility certificates for every fixed entry.
8	`mirror_minimal_counterexample`	Preserve minimal-counterexample status under the specified mirror.
9	`reducible_configuration_exclusion`	Exclude a C-reducible occurrence from a minimal counterexample.
10	`discharge_presentation_soundness`	Prove generic soundness of the concrete finite presentation checker.
11	`degree_5_coverage`	Derive a catalogue occurrence, in either orientation, from a positive degree-5 hub.
12	`degree_6_coverage`	Establish the same semantic occurrence obligation for degree 6.
13	`degree_7_coverage`	Establish the same semantic occurrence obligation for degree 7.
14	`degree_8_coverage`	Establish the same semantic occurrence obligation for degree 8.
15	`degree_9_coverage`	Establish the same semantic occurrence obligation for degree 9.
16	`degree_10_coverage`	Establish the same semantic occurrence obligation for degree 10.
17	`degree_11_coverage`	Establish the same semantic occurrence obligation for degree 11.
18	`discharge_transfer_bound`	Bound each transfer by five under minimality and absence of catalogue occurrences in either orientation.
19	`no_minimal_counterexample`	Assemble the core argument to exclude all minimal counterexamples.
20	`hypermap_four_color`	Assemble four-colorability of every planar bridgeless hypermap.
21	`four_color`	Prove the unchanged finite planar graph root above.

The degree cases quantify over minimal counterexamples with the exact positive score defined by the fixed rules; neighboring degrees have no artificial upper bound. The dependency path uses 16 necessary input targets to derive targets 19, 20 and 21. Targets 6 and 10 support the optional presentation-certificate route. None of targets 19, 20 or 21 is assumed as a shortcut in this assembly.

What completion would provide

The theorem provides a uniform existence guarantee for all finite planar graphs, without a bound on their size. Its Lean development should also make reusable graph embeddings, finite combinatorial maps, coloring transports, and verified finite checkers available to later work.

The existing Rocq development is an executable reference for definitions, dependency structure, and proof behavior. It is not a proof import into Lean. The proposed contribution is a Lean development whose proof objects and computation are justified within Lean's documented foundations. A mechanically translated collection of scripts is not required; contributors should choose abstractions that work well with Mathlib.

Where the difficulty lies

Checking finitely many small graphs does not establish the theorem for arbitrary finite graphs. The development must justify why its finite computational tasks suffice, and must connect their results to the graph statement. The mathematical and computational obligations must meet at explicit, proved interfaces.

There is also a representation gap. The standard target concerns vertex colorings of graphs drawn in the plane, whereas the reference implementation's combinatorial core colors faces of planar bridgeless hypermaps. The latter endpoint is four_color_hypermap in combinatorial4ct.v. Correct treatment of duality, connected components, and isolated vertices is part of the work. Renaming a combinatorial predicate “planar” cannot establish that connection.

Formalization scope and acceptance criteria

Use Lean 4 with a supported, pinned Mathlib revision. The initial draft is checked against Lean v4.30.0 and Mathlib c5ea00351c28e24afc9f0f84379aa41082b1188f. Any later migration must preserve the statements and repeat the relevant checks. Reuse Mathlib's graph and coloring interfaces where appropriate, and develop missing infrastructure as reusable modules. The topological definition must not assume colorability, successful certificate verification, or the conclusion of an intermediate theorem.

The definition layer now provides plane drawings, finite permutation hypermaps, an exact graph/face incidence representation, minimal counterexamples, and rational face charges. Coloring equivalence across a face representation is proved for every positive number of colors, with isolated vertices handled explicitly. Exact Euler equality defines combinatorial planarity; geometric realization is a theorem obligation and cannot be assumed from the name.

The concrete core now defines configurations, ordered boundary traces, contracts, chromograms, Kempe closure, kernel preembeddings and reflected occurrences. The reference reducibility checker has proved soundness and completeness. All 633 maps, rings and contracts are literal data with kernel-validated table/index proofs. The 38 base entries and their 71 symmetrized entries are explicit, and the executable matcher has proved semantic correctness. These infrastructure results do not prove the catalogue's geometric validity, its reducibility, or unavoidability.

The production targets import FourColor.CompactCatalogue.configurations, a compact catalogue containing the same literal maps, rings and contracts. A generic verified decoder constructs validated entries without storing large evaluated proof terms in every import. A separate kernel-checked comparison proves exact ordered equality with the original catalogue, proves that every raw entry is accepted, and proves that none is dropped. The original certificate batches remain available for that audit but are excluded from production target imports. This representation change does not alter any of the 21 mathematical obligations.

Data provenance is pinned to Rocq commit c1d6b1cd5288bea4b067aac13cdde3c18dffe018. Independent fresh-source comparisons check all 633 configurations and every base/expanded rule entry against that snapshot, including actual evaluated Lean payloads. These comparisons establish source correspondence; they are not proofs of reducibility or unavoidability.

The duplicate-data gate rejects unexplained or unintended duplicates and permits verified source-mandated repetition encoding multiplicity or weight. The only repeated rule payload is drule1, deliberately listed twice: the source explains its two-point transfer in discharge.v, lines 17–24 and retains both copies in base_drules (line 145). The Lean rule-match count also counts both copies, preserving weight two. Thus there are 38 base entries with 37 distinct payloads, and 71 expanded entries with 70 distinct payloads. Both copies must remain. No configuration duplicates or other repeated rule payloads are permitted without separately verified source justification.

The reference reducibility evaluator is exponentially expensive. Contributors should implement verified compressed representations or efficient checkers, with acceptance implying the same semantic C-reducibility. Completeness of the reference checker then recovers the stated certificate-existence target. The presentation language is a transparent finite baseline; its generic soundness is an open target, and no completeness claim is made. Source-style quizzes/hubcaps or direct Lean proofs can close the same seven semantic coverage targets. This keeps performance choices separate from the mathematical endpoint.

All computational claims needed by the theorem must be established in Lean. External generators may prepare candidate data or certificates, but their output must be validated by a checker with proved correctness, and the resulting proof must be accepted by the Lean kernel. A recorded successful run of an external program is insufficient. The final theorem and its dependency closure must contain no sorry, admit, unproved custom axiom, or unsupported computational assumption. An axiom audit must identify only Lean/Mathlib's documented foundations. The current 37-declaration conditional/infrastructure audit uses only propext, Classical.choice and Quot.sound; it does not claim an unconditional Four Color proof. Python generators and runtime JSON extraction are outside the mathematical trust boundary and cannot discharge the 21 targets.

Completion requires a reproducible repository in which lake build succeeds from a clean environment and builds the final theorem. Pin toolchain, dependencies, source revisions, and certificate data; document regeneration and verification commands. Maintain a dependency map connecting Lean declarations to exact paper locations and Rocq declarations, and record justified differences in representation. The local multigraph adapter already justifies forgetting parallel-edge multiplicities and transports proper colorings. Any auxiliary restrictions such as connectedness or nonemptiness must be discharged before the root theorem. The current statement and conditional builds verify proposal infrastructure. Success requires proofs of the mission obligations and the final theorem in the reproducible clean build, with no unproved assumptions beyond the documented Lean/Mathlib foundations. All 21 targets remain open at proposal finalization. The submission snapshot records the repository base commit, exact working-file hashes, toolchain, Mathlib revision, payload hashes and audit report; it must not misrepresent uncommitted files as contents of the base commit.

Selected references

Georges Gonthier, A Computer-Checked Proof of the Four Colour Theorem, technical report, 2005. Sections 2–5. Microsoft Research PDF.
Georges Gonthier, Formal Proof—The Four-Color Theorem, Notices of the AMS 55(11), 1382–1393, 2008. Theorem 1 and the formalization architecture. AMS PDF.
Gonthier and Rocq-community contributors, fourcolor, executable formalization, pinned to commit c1d6b1cd5288bea4b067aac13cdde3c18dffe018. Repository.
Neil Robertson, Daniel Sanders, Paul Seymour, Robin Thomas, The Four-Colour Theorem, Journal of Combinatorial Theory, Series B 70(1), 2–44, 1997. DOI; author-hosted manuscript.

54 thms1 active userReviewed

Operations Research Optimization·Captain: mikedeng1

Branch-and-Price-and-Cut for the Split-Delivery Vehicle Routing Problem with Time Windows: Some Optimal Solution Traverses Each Pair of Reverse Customer Arcs at Most OnceResearch Paper

Motivation

Vehicle routing problems ask for minimum-cost vehicle routes that deliver goods from a depot to a set of customers. In the split-delivery vehicle routing problem with time windows (SDVRPTW) a customer's demand may be served by several vehicles, and each customer must be visited inside a prescribed time window. Allowing split deliveries matters in practice: for the variant without time windows, Dror and Trudeau (1989) showed empirically that splitting can save substantially, and Archetti, Savelsbergh and Speranza (2006) proved the savings can reach 50%.

Exact methods for the SDVRPTW are branch-and-price algorithms, and they rely on structural properties of optimal solutions to prune the search. Desaulniers (Operations Research 58(1), 2010) collects these properties in §2 of his paper and uses the strongest one, Corollary 2, as a family of valid inequalities (constraint (7)) in his branch-and-price-and-cut method.

Timeline (as reported by Desaulniers 2010, §§1–2).

1989–1990. Dror and Trudeau prove, for the SDVRP without time windows and with the triangle inequality, that some optimal solution has no two routes sharing more than one split customer.
2006. Gendreau, Dejax, Feillet and Gueguen observe that the property holds with time windows, derive the arc-based Corollary 1, and remark that elementary routes suffice (Remark 1).
2010. Desaulniers strengthens Corollary 1 to pairs of reverse arcs (Corollary 2) and exploits it as cutting planes.

Setting

An instance has $n$ customers $\mathcal N$ , a start depot $0$ and an end depot $n+1$ (the same location at the beginning and end of the planning horizon), and the following data: a vehicle capacity $Q > 0$ ; a demand $d_i > 0$ for each customer, which may exceed $Q$ ; a time window $[e_v, l_v]$ for each node, shared by the two depot copies; nonnegative travel times $t_{vw}$ , which include the service time at $v$ ; and nonnegative costs $c_{vw}$ . The arc set $\mathcal A$ contains the idle arc $(0, n+1)$ and every arc $(v, w)$ , $v \ne w$ , with $e_v + t_{vw} \le l_w$ . The triangle inequality $t_{vx} \le t_{vw} + t_{wx}$ , $c_{vx} \le c_{vw} + c_{wx}$ is assumed throughout.

A route is a walk $0 \to v_1 \to \dots \to v_m \to n+1$ along arcs of $\mathcal A$ , customers possibly repeated, with service start times inside the time windows that respect travel times (waiting is allowed), and nonnegative quantities delivered at its visits whose total is at most $Q$ . Its cost is the sum of its arc costs. A solution is a finite family of routes, one per vehicle, with no bound on their number; it is feasible if every customer $i$ receives in total at least $d_i$ , and optimal if it is feasible and no feasible solution costs less. For customers $i, j$ , let $x_{ij}$ be the number of times arc $(i, j)$ is traversed, summed over all routes of a solution, and let $\mathcal A(\mathcal N) = \mathcal A \cap (\mathcal N \times \mathcal N)$ .

Formalization targets

All four statements assume the triangle inequality and that the instance has a feasible solution, and assert the existence of an optimal solution with a structural property.

Goal: Corollary 2 (p. 181)

\exists \text{ optimal solution with } x_{ij} + x_{ji} \le 1 \quad \text{for all } (i,j) \in \mathcal A(\mathcal N).

The two arcs of a pair of reverse customer arcs are used at most once in total. This is the form constraint (7) of the paper gives to the corollary.

Milestones

Remark 1. Some optimal solution has only elementary routes: no route visits a customer twice.
Theorem 1. Some optimal solution has no two distinct routes with two customers in common.
Corollary 1. Some optimal solution has $x_{ij} \le 1$ for all $(i, j) \in \mathcal A(\mathcal N)$ .

Significance

The result. Corollary 2 turns a property of optimal solutions into linear inequalities on arc-flow variables. Adding them to the arc-flow formulation cuts off fractional points of its linear relaxation while keeping an optimal integer solution, which is how Desaulniers uses them. Remark 1 justifies pricing only elementary routes in column generation. Theorem 1 is the combinatorial fact underneath both corollaries and is reused throughout the split-delivery literature.

Formalizing it. The four results are proved in the literature (Dror–Trudeau; Gendreau et al. 2006); Desaulniers states them without proof. No machine-checked version exists. This mission produces a reusable Lean model of the SDVRPTW (instances, arc sets, feasible routes with schedules and delivery patterns, solutions, optimality) and checked proofs of these properties, including the existence of an optimal solution, which the paper takes for granted.

Difficulty

The obvious argument is local: take an optimal solution that violates the property, shift quantities between two routes, remove a visit, and shortcut. Three points make this less routine than it sounds. First, the statements are existential: each exchange must keep the solution optimal and not reintroduce a violation already removed, so one needs a termination measure that decreases under every exchange (Corollary 2 needs elementarity and the Theorem 1 property simultaneously, not two separate optimal solutions). Second, removing a visit is feasible only because the arc set is defined by time windows: the shortcut arc $(v, w)$ must be shown to exist from the schedule and the triangle inequality on travel times, and the new schedule must be built explicitly. Third, the feasible set is infinite (real quantities, unbounded walks, unbounded number of vehicles), so the existence of an optimal solution is itself a statement to prove, not a hypothesis.

Formalization scope

Namespace SplitDeliveryVRPTW.Known. Nodes are the inductive type Node n (start, cust i for i : Fin n, finish). All quantities, times and costs are real. The arc set is exactly the set the paper defines (read as "if and only if"), with arcs into the start depot and out of the end depot excluded. The triangle inequality for $t$ is imposed on pairwise distinct nodes and for $c$ on triples of arcs, where the paper's data is defined. A route is a customer list (repetitions allowed) with a time function over path positions and a quantity function over visits. A solution is an indexed family Fin m → Route I, so identical routes may appear twice. Demand satisfaction uses $\ge$ , as constraint (2) does. The per-vehicle bound $\min\{d_i, Q\}$ of constraint (14) is omitted because it changes neither the feasible route patterns nor the costs.

Explicit readings of imprecise phrases:

"split customer", "in common" (Theorem 1) are undefined in the paper. A customer two distinct routes visit is split, and the routes have it in common. This visit-based reading is at least as strong as a delivery-based one.
Corollary 2's wording "at most one arc in set $\mathcal A^*_{ij}$ appears at most once" is read through constraint (7): the total number of traversals of the arcs of $\mathcal A^*_{ij}$ is at most one. It is stated in the equivalent form free of the choice of $\mathcal A^*(\mathcal N)$ .
"there exists an optimal solution" is conditional on feasibility, which is the hypothesis added.

Ruled-out trivializations: routes are not restricted to elementary walks (that would make Remark 1 definitional), solutions are not sets (that would forbid duplicate routes), optimality compares against solutions with any number of routes and any visit pattern, "split" is never counted over visits by the same route, capacity and time windows are part of route feasibility, and deliveries occur only at visits.

Useful infrastructure, reusable beyond this mission: shortcut lemmas for feasible routes (removing a visit), exchange lemmas between two routes, and existence of an optimum for split-delivery routing. Contributions of any of these as separate lemmas are welcome.

Selected references

G. Desaulniers, Branch-and-Price-and-Cut for the Split-Delivery Vehicle Routing Problem with Time Windows, Operations Research 58(1):179–192, 2010. https://doi.org/10.1287/opre.1090.0713
M. Dror, P. Trudeau, Savings by split delivery routing, Transportation Science 23(2):141–145, 1989. https://doi.org/10.1287/trsc.23.2.141
M. Dror, P. Trudeau, Split delivery routing, Naval Research Logistics 37(3):383–402, 1990. https://doi.org/10.1002/nav.3800370304
M. Gendreau, P. Dejax, D. Feillet, C. Gueguen, Vehicle routing with time windows and split deliveries, Technical Report 2006-851, Laboratoire Informatique d'Avignon, 2006.
C. Archetti, M. W. P. Savelsbergh, M. G. Speranza, Worst-case analysis for split delivery vehicle routing problems, Transportation Science 40(2):226–234, 2006. https://doi.org/10.1287/trsc.1050.0117

6 thms1 active userReviewed

Graph Theory Operations Research Optimization·Captain: mikedeng1

Scheduling Subject to Resource Constraints: Classification and Complexity III: The Two-Machine Algorithm for Q2 with One Resource and Unit-Time Jobs Is OptimalResearch Paper

Motivation

Many production and computing systems run jobs on parallel machines that also draw on a shared, limited resource: tools, workers, memory, power. Adding such a resource to a scheduling problem can change its complexity entirely. Błażewicz, Lenstra and Rinnooy Kan (DAM 1983) extended the three-field classification $\alpha\mid\beta\mid\gamma$ of Graham, Lawler, Lenstra and Rinnooy Kan by a resource field $res\lambda\sigma\rho$ , and determined the complexity of every problem with unit-time jobs on identical or uniform machines under the makespan criterion. Their Fig. 2 separates the maximal polynomially solvable cases from the minimal NP-hard ones.

This mission formalizes the polynomial side. Two identical machines are easy under arbitrary resources (Theorem 1, due to Garey and Johnson, via maximum matching). Three identical machines with one resource are NP-hard in the strong sense (Theorem 4), and so are two uniform machines with unit resources (Theorem 3). What remains for uniform machines is settled by two algorithms: a sorting-and-shifting procedure for two uniform machines with one resource of arbitrary size (Theorem 5), and a bottleneck transportation problem for any number of uniform machines with one resource and 0–1 requirements (Theorem 6). The hardness results are the subject of the companion missions I and II.

Setting

There are $n$ jobs $J_1,\dots,J_n$ and $m$ machines $M_1,\dots,M_m$ . Machine $M_i$ has speed $q_i>0$ ; every job has unit execution requirement, so it takes time $1/q_i$ on $M_i$ . Identical machines ( $P$ ) have $q_i=1$ ; uniform machines ( $Q$ ) have arbitrary speeds. There are $l$ resources $R_h$ with positive integer sizes $s_h$ , and job $J_j$ needs a nonnegative integer amount $r_{hj}$ of $R_h$ throughout its execution. The field $res\lambda\sigma\rho$ records restrictions: $\lambda$ bounds the number of resources, $\sigma$ their sizes, $\rho$ the requirements, a dot meaning "part of the input". So $res1{\cdot}{\cdot}$ is one resource with arbitrary size and requirements, and $res1{\cdot}1$ is one resource with requirements in $\{0,1\}$ .

A schedule gives every job a machine $\mu(j)$ and a start time $S_j\ge0$ ; the job is executed during $[S_j,C_j)$ with $C_j=S_j+1/q_{\mu(j)}$ . It is feasible if jobs on the same machine do not overlap and, at every time $t$ , the jobs executed at $t$ use at most $s_h$ of each resource $R_h$ . The makespan is $C_{\max}=\max_j C_j$ . No precedence constraints occur in this mission.

Formalization targets

Goal: Theorem 5, correctness of the algorithm

For $Q2\mid res1{\cdot}{\cdot},\,p_j=1\mid C_{\max}$ with $q_1\ge q_2$ : put all jobs on $M_1$ in order of nonincreasing $r_{1j}$ , then repeatedly move the last job of $M_1$ to the earliest feasible time on $M_2$ after the jobs already there, as long as this strictly reduces $C_{\max}$ . For every order with nonincreasing requirements, the resulting schedule $A$ is feasible and

C_{\max}(A)\le C_{\max}(\sigma)\quad\text{for every feasible schedule }\sigma.

Milestones for the goal

The paper's proof has two steps, both milestones. Call a schedule an (a)–(c) schedule when (a) $M_1$ runs its jobs back to back from time $0$ in nonincreasing $r_{1j}$ , (b) $M_2$ runs its jobs in nondecreasing $r_{1k}$ , and (c) every requirement on $M_1$ is at least every requirement on $M_2$ .

The algorithm's schedule is feasible, is an (a)–(c) schedule, and is best among feasible (a)–(c) schedules.
Every feasible schedule can be transformed into a feasible (a)–(c) schedule with no larger $C_{\max}$ .

Further results

Theorem 1. For $P2\mid res{\cdot}{\cdot}{\cdot},\,p_j=1\mid C_{\max}$ , with $G$ the graph joining two jobs when they can run together and $S$ a maximum matching of $G$ , the optimal makespan is $n-|S|$ .
Theorem 6. For $Q\mid res1{\cdot}1,\,p_j=1\mid C_{\max}$ with the $s_1$ fastest machines listed first, the optimal makespan equals the optimal value of a bottleneck transportation problem that assigns jobs to slots (machine, position) with cost $k/q_i$ , resource jobs only to the $s_1$ fastest machines.

Significance

Theorems 5 and 6 complete the classification of Fig. 2 for uniform machines: every special case of $Q\mid res{\cdot}{\cdot}{\cdot},\,p_j=1\mid C_{\max}$ not covered by the hardness theorems has a polynomial algorithm. Theorem 1 is the classical reduction of two-machine resource scheduling to maximum matching, the model case for later work on scheduling with conflict graphs.

The paper proves these results briefly: "clearly" for the first half of Theorem 5, "obviously" for Theorem 1, and a one-paragraph model for Theorem 6. The exchange argument of Theorem 5 is presented "in an informal way" through five steps that pass through fractional, preempted jobs. A machine-checked proof makes these arguments exact on a model with real start times. No formalization of these results is known, and the platform had no statement about resource-constrained scheduling on uniform machines before this mission.

Difficulty

With $q_1\ne q_2$ the job boundaries on the two machines are misaligned: a job on $M_2$ overlaps parts of several jobs on $M_1$ , so the resource check cannot be done slot by slot, and discrete reasoning on integer time grids does not apply. The exchange argument of Theorem 5 must control the resource usage at every real time while jobs are moved between machines and reordered, and it has to end with a nonpreemptive schedule even though the paper's intermediate steps split jobs. For Theorem 1, the hard direction is the lower bound: a feasible schedule with arbitrary real start times must be converted into a matching, which is a statement about how unit jobs on two machines can overlap. For Theorem 6, one must show that restricting resource jobs to the fastest machines and to back-to-back positions loses nothing.

Formalization scope

Model. Jobs, machines and resources are Fin n, Fin m, Fin l (0-based). Speeds are positive reals, sizes positive naturals, requirements naturals. Start times are nonnegative reals, execution intervals are half-open, and the resource constraint is checked at every real time. $C_{\max}=0$ for $n=0$ . The model carries a precedence digraph for consistency with the companion missions; every statement here assumes it has no arcs.
Implicit hypothesis. Theorems 1 and 5 assume every job fits alone ( $r_{hj}\le s_h$ ), which the paper leaves unstated; without it no feasible schedule exists.
The algorithm is a Lean definition following the page: the order is an argument (any nonincreasing order), "as early as possible" is the earliest start after $M_2$ 's last job at which the resource constraint holds throughout, and the loop stops at the first move that does not strictly reduce $C_{\max}$ .
Optimality is always stated in full: feasibility plus a lower bound against every feasible schedule. No minimum is written as an infimum of a possibly empty set.
Theorem 6 is stated with 0–1 slot assignments, the interpretation the paper gives to $x_{ijk}$ ; the page's constraint $\sum_{k=1}^{m}$ is read as $\sum_{k=1}^{n}$ .
Not formalized: the running times $O(ln^2+n^{5/2})$ (Theorem 1), $O(n\log n)$ (Theorem 5, including the phrase "This O(n log n) algorithm") and $O(n^3)$ (Theorem 6), which depend on a machine model the paper does not fix and, for Theorems 1 and 6, on cited matching and transportation algorithms.
Ruled out: a formalization of the goal that proves optimality only against (a)–(c) schedules, against schedules with integer start times, or for one fixed tie-breaking order proves less than Theorem 5.

Contributions welcome: lemmas about step functions of resource usage on half-open intervals, a left-shifting lemma for unit-time schedules on two machines, and the exchange steps of Theorem 5 as separate lemmas.

Selected references

J. Błażewicz, J.K. Lenstra, A.H.G. Rinnooy Kan, Scheduling subject to resource constraints: classification and complexity, Discrete Applied Mathematics 5 (1983) 11–24. https://doi.org/10.1016/0166-218X(83)90012-4
M.R. Garey, D.S. Johnson, Complexity results for multiprocessor scheduling under resource constraints, SIAM Journal on Computing 4 (1975) 397–411. https://doi.org/10.1137/0204035
R.L. Graham, E.L. Lawler, J.K. Lenstra, A.H.G. Rinnooy Kan, Optimization and approximation in deterministic sequencing and scheduling: a survey, Annals of Discrete Mathematics 5 (1979) 287–326. https://doi.org/10.1016/S0167-5060(08)70356-X
S. Even, O. Kariv, An O(n^{2.5}) algorithm for maximum matching in general graphs, Proc. 16th IEEE FOCS (1975) 100–112. https://doi.org/10.1109/SFCS.1975.23

10 thms1 active userReviewed

Completed

Captain: mysticflounder

Eliahou–Revuelta Schur degree: L(4) = 16 and 49 ≤ L(5) ≤ 65Research Paper

Motivation

A set of integers is sumfree when no two of its elements, equal or distinct, add up to an element of the set. The Schur number $S(n)$ is the largest $N$ such that $\{1, \dots, N\}$ can be partitioned into $n$ sumfree sets; only $S(1), \dots, S(5) = 1, 4, 13, 44, 160$ are known. For $n \ge 4$ the best theoretical upper bound that Eliahou and Revuelta could cite in 2021 was $S(n) \le R_n(3) - 2$ , where the Ramsey number $R_n(3)$ is the least $N$ such that every $n$ -colouring of the edges of the complete graph $K_N$ has a monochromatic triangle. The Ramsey numbers satisfy $R_n(3) \le n\,(R_{n-1}(3) - 1) + 2$ for $n \ge 2$ (Greenwood–Gleason 1955); for $S(n)$ the paper knows no recursive upper bound.

Eliahou and Revuelta proposed a conjectural one. They defined a number $L(n)$ through the Schur degree of block-sum sets, proved $S(n) \le n\,L(n)$ (Theorem 5.4) and $S(n-1) + 1 \le L(n) \le R_{n-1}(3) - 1$ (Proposition 5.3), and conjectured $L(n) = S(n-1) + 1$ (Conjecture 5.6). This would give $S(n) \le n\,(S(n-1) + 1)$ (Conjecture 5.7) and $S(6) \le 966$ (Conjecture 5.8), against the range $536 \le S(6) \le 1836$ that they give. For $n = 4$ they proved $14 \le L(4) \le 16$ , conjectured $L(4) = 14$ , and left the value open.

Timeline.

1955: Greenwood and Gleason prove $R_3(3) = 17$ and the recursive bound above.
1961: Baumert computes $S(4) = 44$ (cited by Eliahou–Revuelta as reference [2]).
2000: Fredricksen and Sweet prove $S(6) \ge 536$ (doi).
2004: Fettes, Kramer and Radziszowski prove $R_4(3) \le 62$ (listed in DS1, rev. 18).
2018: Heule proves $S(5) = 160$ with a certified SAT computation (arXiv:1711.08076).
2020–2021: Eliahou and Revuelta, preprint arXiv:2006.01502 and refereed version, with the same numbering of the items used here.
2026: McKenna, The Schur degree of block sums: L(4) = 16 and L(5) ≥ 49 (Zenodo, doi:10.5281/zenodo.22987189), proves $L(4) = 16$ and $L(5) \ge 49$ ; its Lean library ClassicalSchur formalizes both, with $L(5) \le 65$ .

Setting

All numbers are natural numbers, except in the group $G$ below.

Sumfree sets. A set $S$ is sumfree when the sum of two of its elements, equal or distinct, is never in $S$ . A set $X$ is covered by $n$ sumfree sets when it lies in the union of $n$ sumfree sets.

Schur degree. The Schur degree $\operatorname{sdeg}(X)$ is the least $n \ge 1$ such that $n$ sumfree sets cover $X$ . If there is no such $n$ , it is $\infty$ .

For example, $\operatorname{sdeg}(\{1, \dots, N\}) \le n$ holds for $N \le S(n)$ and fails for $N > S(n)$ .

Block sums. Let $A = (a_1, \dots, a_L)$ be a finite sequence of length $|A| = L$ . Its block sums are the sums of runs of consecutive entries:

a_i + a_{i+1} + \dots + a_j \qquad (1 \le i \le j \le L).

The set of these sums is $\hat A$ . The average of $A$ is the rational number $\mu(A) = (a_1 + \dots + a_L)/L$ .

The number $L(n)$ . A length $L$ has the ER property for $n$ when every sequence $A$ of $L$ positive integers with $\mu(A) \le n$ has $\operatorname{sdeg}(\hat A) \ge n$ .

For $n \ge 2$ , the inequality $\operatorname{sdeg}(\hat A) \ge n$ holds when no $n - 1$ sumfree sets cover $\hat A$ . It fails when some $n - 1$ sumfree sets cover $\hat A$ .

The number $L(n)$ is the least $L \ge 1$ with the ER property for $n$ .

The pigeonhole bound. Let $\rho(0) = 2$ and $\rho(k+1) = (k+1)(\rho(k) - 1) + 2$ . The first values are $\rho(1) = 3$ , $\rho(2) = 6$ , $\rho(3) = 17$ and $\rho(4) = 66$ .

For $k \ge 1$ , $\rho(k)$ is an upper bound for the Ramsey number: $R_k(3) \le \rho(k)$ , with equality for $k \le 3$ .

The group $G$ . Let $G = \mathbb{Z}_{m_1} \times \mathbb{Z}_{m_2}$ . A set $C \subseteq G$ is sumfree in $G$ when the sum in $G$ of two of its elements, equal or distinct, is never in $C$ .

The lifted sequence. Take $m_1 \ge 1$ and $M \ge m_1$ . Write the $m_1 m_2$ numbers $u + Mj$ , with $0 \le u < m_1$ and $0 \le j < m_2$ , in increasing order:

x_0 < x_1 < \dots < x_{m_1 m_2 - 1}.

The lifted sequence is the sequence of the $m_1 m_2 - 1$ gaps between consecutive terms, $x_1 - x_0, \dots, x_{m_1 m_2 - 1} - x_{m_1 m_2 - 2}$ . Lemma 4.1 below uses it to turn a cover of $G \setminus \{0\}$ into a sequence in ℕ.

Lean names.

SumFree S: $S$ is sumfree.
CoveredBySumFree X n: $X$ is covered by $n$ sumfree sets.
sdeg X : ℕ∞: the Schur degree, with ⊤ for $\infty$ .
blockSums A and average A, for A : List ℕ: $\hat A$ and $\mu(A)$ .
ERProperty n L: the length $L$ has the ER property for $n$ .
erL n: $L(n)$ .
ramseyBound k: $\rho(k)$ .
GroupSumFree C: $C$ is sumfree in $G$ . The Lean definition takes any type with an addition; the targets use it for ZMod m₁ × ZMod m₂.
liftPrefix m₁ M L: $x_L$ , defined for all $m_1$ and $M$ by $x_L = (L \bmod m_1) + M \lfloor L/m_1 \rfloor$ .
liftSeq m₁ m₂ M: the lifted sequence, defined for all $m_1$ , $m_2$ and $M$ as the list of the $m_1 m_2 - 1$ differences $x_{k+1} - x_k$ .

Formalization targets

Goal

\mathrm{erL}\ 4 = 16

An exact value, so no later result changes the statement; it is the case Eliahou and Revuelta left open.

Theorem 4.1 of Eliahou–Revuelta, in ℕ, with $\rho(k)$ for $R_k(3)$

\rho(k) \le |A| + 1 \implies k + 1 \le \operatorname{sdeg}(\hat A) \qquad (k \in \mathbb{N},\ A \text{ a finite sequence in } \mathbb{N}).

Upper bound of Proposition 5.3, with $\rho(k)$ for $R_k(3)$

\mathrm{erL}(k+1) \le \rho(k) - 1 \qquad (k \in \mathbb{N}).

No length below 16 has the property at $n = 4$

\neg\,\mathrm{ERProperty}\ 4\ L \qquad (1 \le L \le 15).

Lemma 4.1 (McKenna 2026): lift from a group

For $m_1, m_2, q \ge 1$ , $M \ge 3m_1 - 2$ and sets $C_1, \dots, C_q$ , sumfree in $G$ , that cover $G \setminus \{0\}$ , the sequence $A =$ liftSeq m₁ m₂ M satisfies

|A| = m_1 m_2 - 1, \quad a_i > 0, \quad \operatorname{sdeg}(\hat A) \le q, \quad a_1 + \dots + a_L = x_L \ \ (L \le m_1 m_2 - 1).

Corollary 4.2 (McKenna 2026): group coverings bound $L(n)$ from below

For $n \ge 3$ , $m_1, m_2 \ge 1$ and $n - 1$ sets, sumfree in $G$ , that cover $G \setminus \{0\}$ :

m_1 m_2 \le \mathrm{erL}\ n.

Theorem 1.2 (McKenna 2026), with the Lean upper bound: bounds for $L(5)$

49 \le \mathrm{erL}\ 5 \le 65.

Significance

$L(4) = 16$ . At $n = 4$ , Conjecture 5.6 predicts $L(4) = S(3) + 1 = 14$ . So $L(4) = 16$ refutes the conjecture at $n = 4$ . Here $L(n)$ equals the upper bound $R_{n-1}(3) - 1$ of Proposition 5.3.

The two bounds of Proposition 5.3 coincide at $n = 2, 3$ , where the paper gives $L(2) = 2$ and $L(3) = 5$ . So $n = 4$ is the first case in which the conjecture says more than Proposition 5.3.

$L(5) \ge 49$ . At $n = 5$ , Conjecture 5.6 predicts $L(5) = S(4) + 1 = 45$ . So $L(5) \ge 49$ refutes the conjecture at $n = 5$ .

What remains open. Conjectures 5.7 and 5.8 remain open.

The paper derives Conjecture 5.7 at each $n$ from Conjecture 5.6 at the same $n$ , with Theorem 5.4. At $n = 4, 5$ that derivation is not available. But Conjecture 5.7 holds there by the known values: $44 \le 4 \cdot 14$ and $160 \le 5 \cdot 45$ .

Conjecture 5.8 follows from Conjecture 5.6 at $n = 6$ (that is, $L(6) = 161$ ) with Theorem 5.4. Nothing here decides that case.

With $L(4) = 16$ , Theorem 5.4 gives only $S(4) \le 64$ . This is weaker than $S(4) \le R_4(3) - 2 \le 60$ .

Status. Every target is proved and formalized.

Theorem 4.1 and Proposition 5.3 are proved in the refereed paper.
$L(4) = 16$ (Theorem 1.1), Lemma 4.1, Corollary 4.2 and $L(5) \ge 49$ (Theorem 1.2) are proved in McKenna 2026 (doi:10.5281/zenodo.22987189). Before publication, separate agents, with their own code, checked the proofs in two rounds of adversarial audit.

At launch, all 12 theorems of the tree, the goal included, are Proved in Lean over 4 definition bundles. Their only axioms are propext, Classical.choice and Quot.sound.

An independent verifier checked the definitions and the six headline statements against Eliahou–Revuelta and McKenna 2026. The six statements are the goal, Theorem 4.1, Proposition 5.3, Lemma 4.1, Corollary 4.2 and Theorem 1.2.

Literature. The literature search for McKenna 2026 found no result on $L(4)$ , $L(5)$ or Conjectures 5.6–5.8. One citing text, in Jungić 2023, was not read. This records the search; it is not a claim of priority.

Open work, not targets.

The exact $L(5)$ : $49 \le L(5) \le 61$ on paper (with $R_4(3) \le 62$ ), and $49 \le L(5) \le 65$ in Lean.
The case $n = 6$ : $161 \le L(6) \le R_5(3) - 1 \le 306$ (DS1: $R_5(3) \le 307$ ). Here Conjecture 5.6 is the open step toward $S(6) \le 966$ .

Difficulty

Two kinds of bound. The two sides of an exact value of $L(n)$ are statements of different kinds.

An upper bound $L(n) \le m$ needs one length. It follows from $\operatorname{sdeg}(\hat A) \ge n$ for every sequence $A$ of positive integers of one length $L$ , with $1 \le L \le m$ and average at most $n$ .

A lower bound $L(n) \ge m$ needs every shorter length. For every $L$ with $1 \le L < m$ , it needs a sequence of $L$ positive integers, with average at most $n$ , whose block sums are covered by $n - 1$ sumfree sets.

One counterexample at length $m - 1$ is not enough. A sequence of length $L + 1$ and average at most $n$ need not contain $L$ consecutive entries of average at most $n$ . So monotonicity in $L$ does not follow directly from the definition.

The average bound. The lower bound $S(n-1) + 1$ of Proposition 5.3 comes from the constant sequence $(1, \dots, 1)$ , with $\hat A = \{1, \dots, L\}$ . Conjecture 5.6 states that at length $S(n-1) + 1$ , no sequence of average at most $n$ has $\operatorname{sdeg}(\hat A) \le n - 1$ .

Without the bound on the average, this fails. The paper gives a sequence of length 14 with $\operatorname{sdeg}(\hat A) = 3$ , found by semi-random search. Its average is 114, and the authors remark that such examples "are hard to come by".

The gap for $L(5)$ . The gap from 49 to 61 is open. By McKenna 2026 (§5), the construction of Corollary 4.2 gives nothing above 49 at $n = 5$ :

$S(4) = 44$ excludes the cyclic groups of order at least 46.
Solver runs exclude the non-cyclic groups of order 50 to 60. Their unsatisfiability proofs (in the DRAT format) were checked.
$L(5) \le 61$ excludes the orders of 62 or more.

McKenna 2026 knows no sequence of length 49 with average at most 5 and $\operatorname{sdeg}(\hat A) \le 4$ ; such a sequence would give $L(5) \ge 50$ .

Formalization scope

Ambient ℕ. The paper works in an abelian group; here sets are Set ℕ and sequences List ℕ. For $X \subseteq \mathbb{N}$ the Schur degree is the same in ℕ and in ℤ. Theorem 4.1 is formalized for sequences in ℕ only.
sdeg is sInf in ℕ∞, so it is ⊤ when no cover exists, and $\operatorname{sdeg}(\emptyset) = 1$ . Covers are Fin n → Set ℕ; the sets need not be disjoint or inside $X$ . Each lower bound on sdeg must exclude every cover.
blockSums A uses B <:+: A with B ≠ []; average [] = 0 is never used, since erL requires $L > 0$ .
erL n is sInf {L | 0 < L ∧ ERProperty n L} in ℕ, defined for every $n$ (the paper: $n \ge 2$ ). As sInf ∅ = 0, an upper bound on erL alone would hold if no length had the property; the Theorem 4.1 target excludes this, giving ERProperty (k+1) at length $\rho(k) - 1 \ge 1$ , and 0 satisfies neither the goal nor the lower bounds.
Ramsey bound. $\rho(k)$ replaces $R_k(3)$ . TriangleRamsey k N says every colouring of the pairs $x < y$ of at least $N$ naturals with at most $k$ colours has a monochromatic triangle; the tree proves it for $N = \rho(k)$ . As $\rho(4) = 66 > 62 \ge R_4(3)$ , the Lean upper bound for $L(5)$ is 65, not 61.
Lemma 4.1, Corollary 4.2. As in McKenna 2026, the sets need only cover $G \setminus \{0\}$ , and Lemma 4.1 requires $q \ge 1$ : for $q = 0$ , $m_1 = m_2 = 1$ the sequence is empty and $\operatorname{sdeg}(\emptyset) = 1$ . The prefix sums are exact: $x_L$ .
Subtraction is truncated; with $m_1, m_2 \ge 1$ and $\rho(k) \ge 2$ , none of 3 * m₁ - 2, m₁ * m₂ - 1, ramseyBound k - 1 and n - 1 in Fin (n - 1) ( $n \ge 3$ ) truncates, and the differences in liftSeq do not truncate when $M \ge m_1 \ge 1$ .
Finite checks use kernel decide; no native_decide, no external certificate.

Bundles: ClassicalSchurBasic (the objects of the Setting), ClassicalSchurRamsey (TriangleRamsey, ramseyBound), ClassicalSchurLift (GroupSumFree, liftPrefix, liftSeq), ClassicalSchurValues (the finite data of the two value theorems). As a check, the definitions give the paper's values erL 2 = 2 and erL 3 = 5 (checked in Lean by an independent verifier in a scratch file; not in the tree). Reusable: the definitions of ClassicalSchurBasic (the interface lemmas are inlined in the proofs, not separate nodes), TriangleRamsey k (ramseyBound k), and the lift from group coverings. Welcome beyond the targets: a formal TriangleRamsey 4 62, which with not_coveredBySumFree_blockSums gives $L(5) \le 61$ in Lean; the exact $L(5)$ ; the case $n = 6$ .

Selected references

S. Eliahou, M. P. Revuelta, The Schur degree of additive sets, Discrete Math. 344 (2021) 112332. https://doi.org/10.1016/j.disc.2021.112332
S. Eliahou, M. P. Revuelta, The Schur degree of additive sets, preprint, arXiv:2006.01502v1, 2020. https://arxiv.org/abs/2006.01502v1
R. E. Greenwood, A. M. Gleason, Combinatorial relations and chromatic graphs, Canad. J. Math. 7 (1955) 1–7. https://doi.org/10.4153/CJM-1955-001-4
H. Fredricksen, M. M. Sweet, Symmetric sum-free partitions and lower bounds for Schur numbers, Electron. J. Combin. 7 (2000) #R32. https://doi.org/10.37236/1510
M. J. H. Heule, Schur number five, Proc. AAAI-18, 2018; preprint arXiv:1711.08076, 2017. https://arxiv.org/abs/1711.08076
S. P. Radziszowski, Small Ramsey numbers, Electron. J. Combin., Dynamic Survey DS1, revision 18, 2026. https://doi.org/10.37236/21
A. McKenna, The Schur degree of block sums: L(4) = 16 and L(5) ≥ 49, Zenodo, 2026. https://doi.org/10.5281/zenodo.22987189 (version 1.0.1: https://doi.org/10.5281/zenodo.22987688). The Lean library ClassicalSchur and the comparator check: https://github.com/mysticflounder/schur-degree-block-sums (tag v1.0.1).

16 thms1 active userReviewed

Completed

Mathematical Physics·Captain: ShapeZero

Every seven-point Steiner triple system is the Fano plane — so the role postulates force the Fano planeTextbook

Motivation

The Shape Zero model reaches the Fano plane — the seven-point, seven-line configuration behind the seven imaginary units of the octonions — by a combinatorial route: C1 Formal Proofs, §3, Theorem 3.6 ("Roles Force Fano") states that any Steiner triple system admitting a role colouring is the Fano plane. Its proof derives only that there are $7$ points, and takes the last step on trust: C1 §3 asserts "the unique STS(7) (the Fano plane PG(2, 2))" in Theorem 3.3 and justifies it with one sentence, "Uniqueness of STS(7) is classical."

The companion mission The role postulates force exactly seven points proved the point count and deliberately stopped there. This mission supplies the missing step and completes the chain:

Goal: every Steiner triple system on $7$ points is the Fano plane, up to a relabelling of its points.
Capstone: every nonempty Steiner triple system that admits a role colouring is the Fano plane, up to relabelling — C1 Theorem 3.6 in full.

The attack path is the standard textbook proof of the uniqueness of STS(7), supplying the step C1 §3 calls classical. The proof goes through three milestones: a normal form around one point, exactly two completions of it, and an explicit relabelling of each completion onto the Fano plane. The line count (seven lines, three through each point) and the meeting property (any two lines meet in exactly one point) then follow as corollaries of the goal. C1 gives no argument for this step; the milestones below are that classical argument, not C1's.

What this mission does NOT prove.

Not the premise. Why lines have three points and why there are three roles is an input of the model, not derived here.
Not the octonions. The Fano plane is the incidence structure behind the octonion multiplication table, but choosing an orientation and building the multiplication (C1 §4–5: the 16 valid orientations, the 48 role colourings) is a separate step, not covered here.
Up to relabelling only. "Is the Fano plane" means: some bijection of points carries the system's lines exactly onto the Fano plane's lines.

Setting

A Steiner triple system on the points $\{0, \dots, n-1\}$ is a family of $3$ -point subsets, called lines, such that every pair of distinct points lies on exactly one line. A role colouring gives each point of each line one of three roles so that the three points of a line get different roles and every point takes every role exactly once.

The Fano plane is the Steiner triple system on $\{0, \dots, 6\}$ with lines $\{i, i+1, i+3\}$ modulo $7$ :

\{0,1,3\},\ \{1,2,4\},\ \{2,3,5\},\ \{3,4,6\},\ \{0,4,5\},\ \{1,5,6\},\ \{0,2,6\}.

This is the companion mission's published definition RolesForceSeven.fano, labelled $0, \dots, 6$ . (C1 §5 writes the same lines on $e_1, \dots, e_7$ ; this mission uses the companion mission's labelling.)

The definitions RolesForceSeven.STS, RolesForceSeven.RoleColouring and RolesForceSeven.fano are imported from the companion mission, not restated, so both missions refer to the same objects. The one new definition is FanoUnique.IsFano S: there is a bijection $e$ from the points of $S$ to $\{0, \dots, 6\}$ with $\{ e(\ell) : \ell \text{ a line of } S \} =$ the Fano lines.

Formalization targets

Goal: every STS(7) is the Fano plane

S \text{ a Steiner triple system on } 7 \text{ points} \;\Longrightarrow\; \exists\, e \text{ bijective},\quad e(\text{lines of } S) = \text{Fano lines}.

This is FanoUnique.sts7_is_fano.

Milestones — the attack path

M1 (normal form). Every STS on $7$ points can be relabelled so that the lines through point $0$ are $\{0,1,2\}$ , $\{0,3,4\}$ and $\{0,5,6\}$ .
M2 (two completions). If an STS on $7$ $7$ points contains $\{0,1,2\}$ ${0, 1, 2}$ , $\{0,3,4\}$ ${0, 3, 4}$ , $\{0,5,6\}$ ${0, 5, 6}$ , its lines are exactly one of
- A: those three and $\{1,3,6\}, \{1,4,5\}, \{2,3,5\}, \{2,4,6\}$ ;
- B: those three and $\{1,3,5\}, \{1,4,6\}, \{2,3,6\}, \{2,4,5\}$ .
M3 (both completions are the Fano plane). Explicit relabellings carry A and B onto the Fano lines.

The goal follows from M1, M2 and M3. (These are M3, M4 and M5 in the draft's original numbering.)

Corollaries of the goal

A — seven lines, three through each point. An STS on $7$ points has exactly $7$ lines, and every point lies on exactly $3$ of them.
B — two lines meet once. Any two distinct lines share exactly one point.

Both hold in the Fano plane and are preserved by relabelling, so they follow from the goal.

Capstone

For $n \ge 1$ , a Steiner triple system on $n$ points with a role colouring is the Fano plane up to relabelling (FanoUnique.roles_force_fano). The companion mission's goal gives $n = 7$ ; the goal of this mission does the rest. The hypothesis $n \ge 1$ is kept, following the erratum to C1 §3: the empty system satisfies every other condition and is not the Fano plane.

Significance

The result itself. Together with the companion mission, it makes C1 Theorem 3.6 fully machine-verified: the role postulates force not only seven points but the Fano plane itself, up to relabelling.

Formalizing it. C1 cites the uniqueness of STS(7) as classical. It was checked numerically — exhaustively over labelled systems — but never proved in the C1 package; this mission proves it.

Numerical cross-check (exhaustive)

check	result
Steiner triple systems on 7 labelled points	30 (classical count $7!/168 = 30$ )
of those, isomorphic to the Fano plane	30 of 30
any two distinct lines meet in exactly one point	true in all 30
completions of $\{0,1,2\}, \{0,3,4\}, \{0,5,6\}$	exactly 2 (A and B)
swapping points 1 and 2 carries A to B	true

Difficulty

Moderate. M3 is a finite computation. The work is in M1 — building the relabelling bijection from the three lines through a point — and M2, the case analysis on the line through points $1$ and $3$ , which forces the remaining lines. Corollaries A and B follow from the goal by relabelling. Exhaustive search over all line families ( $2^{35}$ ) is not feasible, so the structured proof is needed.

Formalization scope

Points are Fin n; lines are Finset (Fin n); the definitions are the companion mission's, imported unchanged.
"Is the Fano plane" is an equality of line families after relabelling by an equivalence Fin n ≃ Fin 7; it forces $n = 7$ and exactly $7$ lines.
The capstone keeps $0 < n$ and the companion mission's role colouring unchanged.

Selected references

Shape Zero LLC, Formal Proofs of the C1 Verification Package (August 2026), §3 (Theorem 3.3 and Theorem 3.6). https://github.com/ShapeZeroSZ/shape-zero/blob/main/01_source/proofs/ShapeZero_C1_Formal_Proofs.pdf
Errata — C1 Formal Proofs, Section 3 (Theorem 3.6 needs a nonempty point set). https://github.com/ShapeZeroSZ/shape-zero/blob/main/01_source/proofs/ERRATUM_Theorem_6.1.md
Wikipedia, Fano plane. https://en.wikipedia.org/wiki/Fano_plane
Wikipedia, Steiner system. https://en.wikipedia.org/wiki/Steiner_system

10 thms1 active userReviewed

Dynamical Systems Formal Verification·Captain: Rizwan G Mir

Bound L4: 33,070,982 <= R Reversible Binary 2D Moore RulesOpen Problem

Bound $L_4$ : $33,070,982 \le R$

This mission formalizes the lower bound $33,070,982 \le R$ on the number of reversible binary cellular automata on the $3 \times 3$ Moore neighborhood. Extending the conserved-landscape marker families to both centered and off-centered rules.

1 thm1 active userReviewed

Completed

Formal Verification·Captain: Rizwan G Mir

Reversible Binary 2D Cellular Automata: Disproof of R = 18 and Lower Bound R >= 33,076,358Open Problem

Reversible Binary 2D Cellular Automata: Disproof of $R = 18$ and Lower Bound $R \ge 33,076,358$

Problem Statement & Context

A two-dimensional binary cellular automaton (CA) on the infinite grid $\mathbb{Z}^2$ with the standard $3 \times 3$ Moore neighborhood $M = \{-1,0,1\}^2$ updates configurations $c : \mathbb{Z}^2 \to \{0,1\}$ via a local rule $f : \{0,1\}^M \to \{0,1\}$ according to:

F_f(c)(z) = f\Big(\big(c(z + u)\big)_{u \in M}\Big)

A local rule $f$ is reversible (or bijective) if its global map $F_f$ is a bijection of the configuration space $\{0,1\}^{\mathbb{Z}^2}$ .

Let $R$ denote the exact number of reversible binary local rules on the $3 \times 3$ Moore neighborhood. A longstanding open conjecture asserted that $R = 18$ , corresponding solely to the 18 trivial single-cell shifts and complemented shifts:

f(c) = c(z + u) \quad \text{or} \quad f(c) = 1 - c(z + u) \quad (u \in M)

In this mission, we formally disprove $R = 18$ by constructing an explicit non-trivial conserved-landscape rule $f_\star$ whose global map $F_{f_\star}$ is an involution on $\mathbb{Z}^2$ , proving $19 \le R$ . We further extend this result to establish $R \ge 33,076,358$ .

Ladder of Proven Bounds

Bound Level	Proven Bound	Description / Mathematical Mechanism
$\mathbf{L_0}$	$R \ge 18$	Trivial single-cell shifts and complemented shifts ( $2 \times 9 = 18$ ).
$\mathbf{L_1}$	$R \ge 19$	Disproof of $R = 18$ via explicit non-trivial conserved-landscape rule $f_\star$ .
$\mathbf{L_2}$	$R \ge 33,070,982$	Conserved-landscape marker rule family ( $24,576$ centered rules).
$\mathbf{L_3}$	$R \ge 33,076,358$	Incorporation of $5,376$ off-centre marker rules reading center cell $x_0$ .
Symmetry	$R_{\text{rot90}} = 74$	Exactly 74 rules invariant under $90^\circ$ spatial rotations.
Torus	$	\mathcal{R}_{2,3}
Upper Limit	$R \le 2^{511}$	Derived from constant divergence condition $f(\mathbf{0}) \ne f(\mathbf{1})$ .

Key Milestone Theorems

Theorem 1 (Trivial Rule Reversibility): All 18 single-cell shift and negated-shift rules are bijective global maps.
Theorem 2 (Conserved-Landscape Involution $f_\star$ ): The rule $f_\star$ complements a cell iff its W and SE neighbors are $1$ and the other six are $0$ . $F_{f_\star} \circ F_{f_\star} = \text{id}$ .
Theorem 3 (Non-Triviality & $19 \le R$ ): $f_\star$ differs from every trivial rule, establishing $19 \le R$ and disproving $R = 18$ .
Theorem 4 (Constant Divergence Condition): Every reversible rule satisfies $f(\mathbf{0}) \ne f(\mathbf{1})$ .

7 thms1 active userReviewed

Completed

Number Theory·Captain: moutei

Erdős #131: the ELRSS bound F(N) < 3·sqrt(N) + 1 (the open problem itself is NOT settled)Open Problem

What this mission proves, and what it does not. The goal theorem is the explicit upper bound $F(N)<3\sqrt N+1$ of Erdős, Lev, Rauzy, Sándor and Sárközy (1999) — a published result, now formally verified here. Erdős problem #131 itself is NOT solved by this mission. Erdős asked for the order of growth of $F(N)$ , which is known only to lie between $N^{1/5}$ and $N^{1/4+o(1)}$ and remains open. A goal theorem reading Proved therefore means the 1999 bound is formalized, nothing more.

Motivation

Call a finite set of positive integers non-dividing if no element of it divides the sum of any nonempty collection of the other elements. The condition is easy to state and immediately restrictive: taking the collection to be a single element already forbids $a \mid b$ , so a non-dividing set is primitive, and taking larger collections forbids a great deal more. Paul Erdős asked, with Lev, Rauzy, Sándor and Sárközy, how large such a set can be inside $\{1,\ldots,N\}$ . Writing $F(N)$ for that maximum, the question is to determine the order of growth of $F(N)$ . It remains unanswered, and the gap between what is known from above and from below is a full factor of $N^{1/20}$ .

The problem sits at the meeting point of divisibility and additive combinatorics. Its upper bounds come from the theory of non-averaging sets, since every non-dividing set is non-averaging; its lower bounds come from explicit constructions. The two sides have been improved independently for twenty-five years without meeting.

Setting

Work inside $\mathbb{N}$ . For a finite $A \subseteq \mathbb{N}$ and $a \in A$ , write $A \setminus \{a\}$ for $A$ with $a$ removed. Say that $A$ is non-dividing when

\forall a \in A,\ \forall S \subseteq A \setminus \{a\} \text{ with } S \neq \emptyset:\qquad a \nmid \sum_{x \in S} x .

Two conventions are forced. First, $S$ ranges over all nonempty subsets, singletons included, so primitivity is part of the property rather than an extra assumption. Second, $S$ must be nonempty: the empty sum is $0$ and every $a$ divides $0$ , so admitting $S = \emptyset$ would leave no non-dividing sets at all.

Define the extremal function

F(N) \ =\ \max\{\,|A| \ :\ A \subseteq \{1,\ldots,N\},\ A \text{ non-dividing}\,\}.

A set is non-averaging if no element equals the average of some nonempty collection of the others. Every non-dividing set is non-averaging, which is the link through which the strongest upper bounds arrive.

Target

The goal is the explicit upper bound of Erdős, Lev, Rauzy, Sándor and Sárközy:

F(N) \ <\ 3N^{1/2} + 1 .

The question Erdős actually posed is stronger and remains open:

\textbf{Determine the order of growth of } F(N).

Significance

The bound above is the sharpest explicit constant in the literature, and it is the natural formalization target: it is a clean closed-form inequality valid for every $N$ , with a self-contained combinatorial proof, and nothing about it is asymptotic.

Beyond it lies the open question. What is known:

$F(N) > \exp\!\big((\sqrt{2/\log 2} + o(1))\sqrt{\log N}\big)$ , due to Straus, which refuted Erdős's own initial guess that $F(N) < (\log N)^{O(1)}$ .
$F(N) \gg N^{1/5}$ , from a construction Erdős credits to Csaba.
$F(N) < 3N^{1/2} + 1$ , the target above.
$F(N) \le N^{1/4 + o(1)}$ , from Pham and Zakharov's theorem on non-averaging sets. This settles Erdős's specific sub-question — whether $F(N) > N^{1/2 - o(1)}$ — in the negative.

So the truth lies between $N^{1/5}$ and $N^{1/4+o(1)}$ , and which end is right is unknown.

Difficulty

The obvious argument gives almost nothing. Pigeonhole on partial sums shows $|A| \le \min A$ : order the other elements arbitrarily, form the running sums, and if there are more of them than residues modulo $\min A$ then two agree, making a contiguous block sum divisible by $\min A$ . That is genuinely all the elementary argument yields, and it is compatible with $|A|$ as large as $N$ .

The difficulty is that the constraint is a statement about exponentially many subset sums, while the conclusion is about a single cardinality. Every strong bound known proceeds by discarding almost all of that information and keeping a structured fragment — contiguous blocks, or the averaging condition — and the loss at that step is exactly what separates $N^{1/5}$ from $N^{1/4}$ . Improving either side appears to require using the divisibility conditions for several elements $a$ simultaneously, which no current argument does.

Formalization scope

Sets are Finset ℕ. The forbidden subsets are drawn from A.erase a, so the tested element never appears in the sum it is tested against, and they are quantified as members of (A.erase a).powerset rather than by the subset relation, which makes the property decidable — this is what allows an explicit finite witness to be checked by the kernel rather than asserted. $F(N)$ is a Finset.sup of cardinalities over the filtered powerset of Finset.Icc 1 N, so it is a total function with no junk-value caveats and lower bounds on it follow from exhibiting a single set.

The target inequality is stated over ℝ with Real.sqrt, matching the source's $3N^{1/2}+1$ rather than any integer rounding of it.

Timeline

1980s–1998. Erdős poses the problem repeatedly, initially conjecturing $F(N) < (\log N)^{O(1)}$ .
Straus. Disproves that guess, with $F(N) > \exp(c\sqrt{\log N})$ .
Csaba. A construction giving $F(N) \gg N^{1/5}$ , credited by Erdős in 1997.
1999. Erdős, Lev, Rauzy, Sándor and Sárközy name the property non-dividing and prove $F(N) < 3N^{1/2} + 1$ .
2024. Pham and Zakharov bound non-averaging sets, yielding $F(N) \le N^{1/4+o(1)}$ and answering Erdős's sub-question negatively.
Open. The order of growth of $F(N)$ , anywhere between $N^{1/5}$ and $N^{1/4+o(1)}$ .

Selected references

P. Erdős, V. Lev, G. Rauzy, C. Sándor, A. Sárközy, Greedy algorithm, arithmetic progressions, subset sums and divisibility, Discrete Mathematics 200 (1999), 119–135.
H. T. Pham, D. Zakharov, Sharp bound for the Erdős–Straus non-averaging set problem, arXiv:2410.14624; Geom. Funct. Anal. (2025). Theorem 1: a non-averaging $A\subseteq[n]$ has $|A|\le n^{1/4+o(1)}$ .
R. K. Guy, Unsolved Problems in Number Theory, 3rd ed., Springer (2004), problem C16.
Erdős problem #131, https://www.erdosproblems.com/131
OEIS A068063, Maximum cardinality of a nondividing subset of $\{1,\ldots,n\}$ .

16 thms1 active userReviewed

Discrete Geometry·Captain: mikedeng1

Convex Polytopes V.5: Effective enumeration of combinatorial typesTextbook

A convex polytope has both geometric coordinates and a finite pattern of faces. Moving its vertices can change distances and angles while preserving which vertices belong to which faces. Enumeration by combinatorial type asks for those incidence patterns, with geometrically different realizations of the same pattern counted together. Grünbaum’s enumeration theorem establishes that the complete collection can be determined algorithmically when the dimension and number of vertices are prescribed Convex Polytopes, §5.5, p.91.

A d-polytope here is a nonempty convex hull of finitely many points in real d-dimensional coordinate space, with affine span equal to the whole space. A face is obtained by maximizing a linear functional over the polytope; the collection of faces also includes the empty face and the polytope itself. Inclusion orders this collection. Two polytopes have the same combinatorial type when their full face collections admit an order isomorphism. This notion retains the incidence structure and forgets metric measurements.

To describe a type with finite data, label the k vertices by the integers from zero through k−1. Record the set of vertex labels belonging to each nonempty proper face. This family of subsets is the polytope’s scheme. A finite list of finite lists of natural numbers encodes such a family. The order of labels and repeated occurrences of a label do not change the represented subset. A scheme is realized only when its recorded subsets are exactly the vertex sets of the nonempty proper faces: it cannot add faces, omit faces, or introduce labels outside the prescribed range.

The target is a single total computable function

E : \mathbb N\times\mathbb N\longrightarrow \operatorname{List}(\operatorname{List}(\operatorname{List}(\mathbb N))).

For every dimension d and vertex count k, each scheme in E(d,k) must have a realizing d-polytope with exactly k vertices. Every d-polytope with k vertices must realize some scheme in that output. Finally, if polytopes realizing two output positions have isomorphic full face posets, those positions must be equal. These requirements say that the output contains precisely one representative of every combinatorial type. The existential choice of one function precedes both numerical inputs, so the algorithm must work uniformly for all dimensions and vertex counts.

The result supplies an effective finite classification at each prescribed size. It is stronger than the observation that only finitely many incidence families can be written down: those families need not all arise from real convex polytopes. It also addresses termination, since a total algorithm must return its entire finite answer for every input. The theorem is a known mathematical result in the cited textbook. The present formal target asks for a proof of its stated algorithmic conclusion; no machine-checked proof of that conclusion is asserted here.

The principal difficulty is the connection between finite incidence data and geometric realizability. Combinatorial consistency alone does not supply real coordinates for a convex polytope. The source distinguishes this realizability question from the enumeration conclusion and identifies decidability over the real numbers as relevant to it §5.5, p.91. The mission retains the complete enumeration conclusion, including realizability of each answer, coverage of every type, and absence of duplicate types.

The formal representation uses real coordinates without a rationality restriction and permits nonsimplicial polytopes. Vertices are labelled injectively and exhaustively. The number of vertices is expressed as the number of nonempty zero-dimensional exposed faces. Nonemptiness separates the empty face, whose book dimension is −1, from the natural-valued dimension used to count faces. For finite convex hulls the face collections are finite, so this cardinality has its usual meaning.

Natural-number dimensions include dimension zero. The unique point has one vertex and no nonempty proper faces, and therefore uses an empty scheme. This is an explicit extension of the source’s positive-dimensional scheme convention. Unrealizable dimension and vertex-count pairs require an empty output. Finite-polytope faces, their ordered collection, vertex counts, and finite scheme realizations are the concrete objects needed to state the goal; total computability applies to the complete finite output rather than to individual tests alone.

Reference: Branko Grünbaum, Convex Polytopes, second edition, Springer, 2003, §5.5, Theorem 2 (5.5.2), printed p.91, PDF p.117; definitions in §§2.4 and 3.1. Source text.

5 thms1 active userReviewed

Discrete Geometry·Captain: mikedeng1

Convex Polytopes IV: Facet growth of binary polytopes (GRU-M04-BINARY-EXTREMA)Textbook

Binary choices and polyhedral complexity

A vector whose coordinates are all zero or one records a collection of yes-or-no choices. Taking the convex hull of a collection of these vectors gives a 0/1-polytope, also called a binary polytope. Such objects connect discrete choices with geometry: points describe feasible combinations, while supporting inequalities describe restrictions that every feasible combination satisfies. Grünbaum's discussion in §4.9 emphasizes the role of facets of these polytopes in combinatorial optimization and cutting-plane descriptions.

The question here concerns how many facets can occur when the dimension grows. Restricting every generating point to binary coordinates gives a finite, highly structured collection of possible points. Nevertheless, this restriction still allows polytopes with very many distinct boundary faces. The theorem of Bárány and Pór establishes superexponential growth in the largest possible number of facets. The mission concerns the form of this growth asserted in Grünbaum's 2003 notes, printed page 69a, rather than a prescribed numerical constant.

Polytopes, dimension, and facets

Fix a natural number d. The ambient space is the real coordinate space R^d. A convex hull consists of all convex combinations of the generating points, meaning weighted averages with nonnegative weights whose sum is one. A polytope is the convex hull of a finite set of points. It is full-dimensional when its affine span is all of R^d; this rules out a polytope lying in a proper affine subspace.

For a binary polytope, every generating point belongs to {0,1}^d. A subset of this cube is automatically finite. Nonemptiness and full dimension are imposed separately in the target. Consequently, the dimension in the facet bound is the actual dimension of the polytope as well as the dimension of its coordinate space.

An exposed face is the set of all points of the polytope that maximize a given linear functional. A facet is a face of affine dimension d−1. Facets are counted as geometric sets. Two different inequalities that expose the same face do not contribute two facets. Write f_(d−1)(P) for this number.

The growth target

The target is the following existence statement:

\exists c>1\;\exists D\in\mathbb N,\ D\ge2,\quad \forall d\ge D\;\exists P\subseteq\mathbb R^d,\quad P\text{ is a full-dimensional binary polytope},\qquad f_{d-1}(P)>c^{d\ln d}.

The constant c and threshold D are chosen before the dimension d. The polytope P may depend on d. The assertion therefore supplies a witness in every sufficiently large dimension. It does not merely assert the existence of one complicated polytope or of witnesses along an unspecified subsequence.

The logarithm is natural. Replacing it by another fixed base greater than one changes the admissible constant c, while preserving the shape of the theorem. The statement leaves both c and D unspecified. The Bárány–Pór paper, Theorem 1.1, supplies the asymptotic context for the book's formulation.

What superexponential growth says

For any fixed c greater than one, the expression c^(d ln d) eventually exceeds A^d for every fixed A greater than one. Thus a single exponential base cannot bound the facet counts of all binary polytopes across dimensions. The binary-coordinate restriction alone does not yield that kind of uniform bound.

The underlying mathematical result is established in the literature. The formalization task is to prove its stated existence conclusion with the precise geometric definitions above. The conclusion concerns actual facets of actual polytopes, so a family of redundant inequalities or a list with repetitions would not satisfy the counting requirement.

Why the existence statement is demanding

A large supply of binary points does not by itself identify the supporting hyperplanes of their convex hull. Counting points and counting facets are different tasks. Moreover, the theorem requires the same growth constant across all sufficiently large dimensions. Verifying individual examples, even examples with many facets, leaves that uniform asymptotic requirement unresolved.

The book describes certain random polytopes as witnesses. Its stated conclusion gives no probability distribution or numerical probability bound. The target records the resulting extremal existence assertion; it imposes no extra probabilistic hypothesis on the witness.

Geometric conventions

The coordinate model is Fin d → ℝ. IsDPolytope requires a nonempty finite convex hull with full affine span. IsZeroOnePolytope specifies the hull of binary-coordinate points. faceCount P k counts nonempty exposed faces with affine dimension k. These concrete notions also apply to other questions about finite-dimensional polytopes.

Face counts use natural cardinality. On the domain of finite polytopes there are only finitely many faces, so this is the ordinary finite count. Requiring D at least two ensures that d−1 represents the facet dimension without a low-dimensional subtraction convention and that the logarithm's argument is positive. Full dimension excludes the whole polytope from the facet count, and nonemptiness excludes the empty face.

Selected references

Branko Grünbaum, Convex Polytopes, second edition, Springer, 2003, §4.9, printed p.69a; definitions in §§2.4 and 3.1. Book.
Imre Bárány and Attila Pór, On 0-1 Polytopes with Many Facets, Advances in Mathematics 161 (2001), 209–228, Theorem 1.1. Paper.

2 thms1 active userReviewed

Discrete Geometry·Captain: mikedeng1

Convex Polytopes V: Recognition from projections (GRU-M05-PROJECTION-RECOGNITION)Textbook

Recognizing a convex set from its projections

A convex set can be studied through its images in spaces of smaller dimension. Each image records part of the geometry, while losing the information along the directions that are collapsed. A finite convex hull always has finite convex hulls as its affine images. The converse asks whether sufficiently rich projection data can force the original set to have a finite description by points. This mission concerns the recognition theorem attributed to Klee in Grünbaum's Convex Polytopes, §5.1, Theorem 8, printed page 74.

The question concerns all projections into a suitable dimension, rather than an individual view of a set. A single image may conceal directions in which the original set has additional structure. The theorem identifies a condition on the entire family of images that characterizes polytopes among bounded convex sets.

Sets, convex hulls, and affine projections

Fix an integer $d\geq3$ . Real coordinate space $\mathbb R^d$ consists of vectors with $d$ real coordinates. A set $K\subseteq\mathbb R^d$ is convex if it contains the line segment joining any two of its points. It is bounded if its points remain within some finite distance of the origin. Neither condition requires $K$ to fill the ambient space.

The convex hull of a set $V$ , written $\operatorname{conv}(V)$ , is the smallest convex set containing $V$ . A polytope is the convex hull of a finite set. The generating set need not be a minimal set of vertices. Grünbaum gives this characterization in §3.1, printed page 31. The empty generating set is permitted, as are generating sets contained in a proper affine subspace.

An affine map preserves affine combinations. A surjective affine map $f:\mathbb R^d\to\mathbb R^j$ has a $j$ -dimensional target and reaches every point of that target. When $j<d$ , such a map loses dimensions. This represents the singular affine images called projections in §5.1, printed page 71, with coordinates chosen on the target affine space. Translation of the target is allowed.

The recognition target

For every bounded convex set $K\subseteq\mathbb R^d$ , the goal is the equivalence

K\text{ is a polytope} \quad\Longleftrightarrow\quad \exists j\in\mathbb N,\quad 2\leq j<d,\quad \forall f:\mathbb R^d\twoheadrightarrow\mathbb R^j\text{ affine},\quad f(K)\text{ is a polytope}.

The dimension $j$ may depend on $K$ , but it is chosen before testing the affine maps. Every surjective affine map with that target dimension is tested. For each such map, the finite set generating the image can be different. No common set of projected vertices or uniform bound on the number of generators is required.

This is one recognition theorem, containing both implications. The selected source grouping does not introduce separate supporting theorem targets.

What the criterion establishes

The theorem characterizes a global finite convex-hull property through lower-dimensional images. In particular, the conclusion concerns the original set itself; it does not merely assert that its closure has a finite generating set. This distinction matters because boundedness and convexity alone do not assert closedness.

The result is a known mathematical theorem in the source. The formalization target is its complete equivalence with the stated domain and quantifier order. A proof of only the preservation of polytopes under affine maps would leave the recognition implication unresolved.

Why the converse requires more than one image

Every tested image can have its own finite generating set. Finiteness of each image does not directly supply a finite generating set that works in the original ambient space. The recognition implication must connect the universal family of images to the geometry of the whole set. Replacing that family by a convenient fixed projection would change the question.

Mathematical conventions

Real $d$ -space is represented by functions from Fin d to the real numbers. Boundedness and convexity use the ordinary Mathlib predicates, and being a polytope is expressed directly by existence of a finite set with the specified convex hull. No full-dimensional polytope structure is imposed on $K$ .

The hypothesis $d\geq3$ makes explicit the admissible ambient dimension needed for $2\leq j<d$ . In dimension three, the only available target dimension is two. No assertion of the displayed existential criterion is made in dimensions zero, one, or two. Empty sets, singleton sets, and other lower-dimensional subsets remain within the domain in every admissible ambient dimension.

Affine maps are required to be surjective onto the selected coordinate space. Thus their rank is exactly the selected target dimension, rather than an accidentally smaller rank. Closedness, nonemptiness, rational coordinates, and a predetermined number of vertices are not additional hypotheses. The mathematical ingredients are real convex hulls, finite sets, bounded sets, and affine images.

Selected references

Branko Grünbaum, Convex Polytopes, second edition, Springer, 2003. Theorem 5.1.8, printed page 74 (source.pdf page 100); projection convention, printed page 71 (PDF97); polytope convention, printed page 31 (PDF51). The source pages are included in this package's evidence directory.

1 thm1 active userReviewed

Discrete Geometry·Captain: mikedeng1

Convex Polytopes V: Simplex sections through prescribed points (GRU-M05-PRESCRIBED-SECTIONS)Textbook

A polytope can be represented by cutting a higher-dimensional simplex with an affine flat. The geometry of the cut determines the resulting polytope. Perles's prescribed-point theorem adds a constraint to this representation: the cutting flat must pass through a point chosen in advance inside the simplex. Theorem 5.1.10 in Branko Grünbaum's Convex Polytopes, second edition (2003), shows that this requirement can always be met when the simplex has enough facets. The source is §5.1, printed page 74, with the section convention introduced on printed page 71.

A polytope is the convex hull of finitely many points. In this mission it is nonempty and full-dimensional in its ambient real coordinate space. Thus a d-polytope P in R^d contains enough points to span that space affinely. A face is the set of points on which a supporting linear functional attains its maximum; a facet is a face of dimension d−1. Different supporting functionals can describe the same face, so the facet allowance counts geometric faces rather than inequalities used to describe them.

A k-simplex is the convex hull of k+1 affinely independent points. Write its vertices as v₀,…,vₖ in R^k and its convex hull as T. Affine independence means there is no nontrivial affine relation among these vertices. The simplex therefore has dimension k, and its interior is taken in the whole space R^k. No restriction is placed on its side lengths or angles. A d-flat is a translate of a d-dimensional linear subspace. A section of T by such a flat L is the entire intersection T ∩ L.

The target is the following existence assertion. For every d-polytope P with at most k+1 facets, every k-simplex T in R^k, and every p in the interior of T, there is a d-flat L such that

p\in L,\qquad T\cap L\text{ is affinely equivalent to }P.

An affine equivalence here preserves affine combinations and is invertible on the affine spans. It can change lengths and angles. In the stated coordinates, it is represented by an injective real affine map A from R^d onto L satisfying

A(P)=T\cap L.

All input data, including the interior point p, are universally quantified before the flat and map are chosen. The flat can depend on these data. The source writes the facet allowance as f and the simplex dimension as f−1; the notation here uses f=k+1.

The prescribed-point conclusion gives control beyond the existence of some simplex section representing P. It permits the simplex and an interior point to be fixed while the cutting flat is selected to recover the given polytope. The conclusion concerns its full affine geometry: the image of every point of P lies in the section, and every point of the section belongs to that image. This is the additional representational constraint discussed immediately before Theorem 10 on printed page 74.

The difficulty lies in meeting these requirements simultaneously. A flat through the chosen point can have an intersection of the wrong affine shape. A section with the correct affine shape need not contain the prescribed point. The theorem requires both properties for every allowed simplex and point, while retaining the original facet bound. Neither a special regular simplex nor a selected interior point captures this quantifier structure.

The formal statement uses real coordinate spaces indexed by finite sets, finite convex hulls, affine spans, exposed faces, and affine maps. Nonempty faces are counted by their affine dimension. In dimension zero the facet allowance is automatic: under the convention counting the empty face it contributes at most one facet, which fits the allowance k+1. This avoids interpreting natural subtraction d−1 as a facet dimension at d=0. The zero-dimensional simplex and zero-dimensional polytope remain within the statement.

This is a known geometric theorem whose formal proof remains to be supplied. The target contains one proof placeholder. The definitions specify the underlying geometry concretely. The mission consists of the single prescribed-section theorem; its definitions support that statement, and no separate supporting theorem is included as a milestone. The source is Grünbaum, Convex Polytopes, second edition, Springer, 2003, §5.1, Theorem 10, printed page 74 (source.pdf page 100); see also §5.1, printed page 71 (PDF page 97), for the section convention.

3 thms1 active userReviewed

Discrete Geometry·Captain: mikedeng1

Grünbaum — Gale data and combinatorial type (5.4.5)Textbook

Gale data and combinatorial type

A convex polytope has geometric coordinates and a combinatorial structure: its faces, ordered by inclusion. Different coordinates can describe the same combinatorial type. Gale transforms connect these viewpoints by encoding affine dependencies among the vertices as another point configuration, often in a smaller-dimensional space.

Let P and Q be full-dimensional d-polytopes in real coordinate space, each with n vertices. Choose injective lists V and W containing all their vertices and fix a permutation θ of the n indices. The question is whether this prescribed vertex correspondence extends to an isomorphism between the full face posets of P and Q. The empty face and the whole polytope are included in these posets.

An affine dependency of V is a list of real coefficients a whose sum is zero and whose weighted sum of the vertices is zero. These coefficient lists form a vector space of dimension n−d−1. Choose any basis and put its vectors into the columns of a matrix. The n rows of this matrix form a Gale transform G of V. A Gale transform H of W is constructed in the same way, with its own choice of basis. The rows may repeat and may be zero; there is no general-position assumption.

Theorem 5.4.5 states that the prescribed correspondence extends to an isomorphism of face posets exactly when it preserves every relative-interior test on the Gale configurations. For every subset J of vertex indices, the origin belongs to the relative interior of the convex hull of the rows G(J) if and only if it belongs to the relative interior of the convex hull of H(θ(J)). Relative interior means interior within the affine span of the selected convex hull, not interior in the whole coordinate space.

The equivalence concerns every subset of indices and both directions of implication. It retains the prescribed permutation rather than merely asking whether the polytopes have some combinatorial equivalence. Indexing the Gale points also keeps track of which original vertices they represent when several Gale rows coincide. Taking a set image does not change the convex hull of a chosen subconfiguration.

The empty subset is included: its convex hull has empty relative interior, so both membership tests are false. For a simplex, n=d+1 and the Gale space has dimension zero. Its nonempty row subconfigurations consist of the zero vector, and the relative-interior formulation still applies. Zero-dimensional polytopes are also retained.

This mission is the equivalence criterion itself, with the concrete definitions of a full-dimensional polytope, its face poset, and a Gale transform. The grouping keeps transform construction within the vocabulary of the criterion. The neighboring results on affine and projective equivalence have different conclusions and are outside this goal.

Source: Branko Grünbaum, Convex Polytopes, second edition (2003), §5.4, Theorem 5, printed page 89 (PDF page 115). The affine-dependence construction appears on printed pages 85–86 (PDF pages 111–112).

4 thms1 active userReviewed

Combinatorics

Missions

Periodic Multidimensional Costas Arrays (Rubio–Torres Conjecture 1)Open Problem

Motivation

Setting

Formalization target

Significance

Difficulty

Formalization scope

Selected references

The Strong Perfect Graph Theorem I: A Graph Is Perfect If and Only If It Is BergeResearch Paper

Motivation

Setting

Formalization targets

Theorem 1.2: perfection and the Berge property

Structural and reduction milestones

Significance

Difficulty

Formalization scope

Selected references

Six-colour Schur colourings of [1, 1801] under R₄(3) ≤ 61: balanced classes, nested saturation and forced reflectionResearch Paper

Motivation

Setting

Formalization targets

Goal: six colours under R4(3)≤61R_4(3) \le 61R4​(3)≤61

Centred-interval bound

Balanced colour classes

Nested saturation

Automorphism extension

Forced reflection

The saturation degree is even

Significance

Difficulty

Formalization scope

Selected references

Project Scheduling with Time Windows and Scarce Resources IV: Every Feasible Schedule Obeys a Minimal Delaying Mode of Each Forbidden SetTextbook

Motivation

Setting

Formalization targets

Goal: Theorem 2.5.7 (p. 49)

Milestones

Significance

Difficulty

Formalization scope

Selected references

Project Scheduling with Time Windows and Scarce Resources II: A Time-Feasible Strict Order Is Feasible iff It Breaks Up Every Minimal Forbidden SetTextbook

Motivation

Setting

Formalization targets

Goal: Theorem 2.3.10 (Bartusch et al. 1988)

Milestones

Significance

Difficulty

Formalization scope

Selected references

An Introduction to the Theory of Mechanism Design IX: Monotone Direct Mechanisms Are Dictatorial (Gibbard–Satterthwaite)Textbook

Motivation

Setting

Formalization targets

Goal: Proposition 8.5 (Muller–Satterthwaite)

Milestones

Significance

Difficulty

Formalization scope

Selected references

Linear Programming: Foundations and Extensions III: Network Flows, the Integrality Theorem and König's TheoremTextbook

Motivation

Setting

Formalization targets

Goal: König's Theorem (Theorem 14.3, p. 216)

Milestones

Significance

Difficulty

Formalization scope

Selected references

Discrete Convex Analysis XIV: The König-Egerváry Theorem for Mixed MatricesTextbook

Motivation

Setting

Formalization targets

Significance

Goal: six colours under $R_4(3) \le 61$

Goal: Theorem 1.8, under $|\sigma_n|\to\infty$