Graph Theory

Completed

Operations Research·Captain: Shuze Chen

Dynamic Programming and Optimal Control II: Label Correcting MethodsTextbook

Motivation

Label correcting methods are the workhorse family of shortest-path algorithms — Dijkstra's method, Bellman–Ford, SLF/LLL variants and A* all fit the template analyzed in §2.3.1 of Bertsekas, Dynamic Programming and Optimal Control, Vol. I (3rd ed., 2005), where shortest paths appear as the purely deterministic face of dynamic programming. The correctness proof (Prop. 2.3.1) is short on paper but genuinely nondeterministic — any node may be removed from the candidate list, children processed in any order — so a formal proof certifies a whole family of concrete algorithms at once.

Setting

A finite directed graph with arc set $\mathcal{A}$ , real arc lengths $a_{ij}$ , origin $s$ and destination $t \ne s$ (BertsekasSPGraph). Walks are nonempty node lists whose consecutive pairs are arcs (BertsekasIsWalkFrom), with length the sum of arc lengths (BertsekasWalkLength); the shortest distance is the infimum of walk lengths in the extended reals, $+\infty$ if no walk exists (BertsekasShortestDistance). The standing assumption of §2.3: every cycle has nonnegative length (negative arcs allowed).

The algorithm state (BertsekasLCState) carries labels $d_j \in \overline{\mathbb{R}}$ , the scalar UPPER, and the candidate list OPEN. Initially $d_s = 0$ , all other labels $\infty$ , UPPER $= \infty$ , OPEN $= \{s\}$ . One iteration (BertsekasLCStep, nondeterministic): remove any $i$ from OPEN; for each child $j$ of $i$ in any order, if $d_i + a_{ij} < \min\{d_j, \text{UPPER}\}$ set $d_j := d_i + a_{ij}$ , and put $j$ in OPEN if $j \ne t$ , or update UPPER if $j = t$ . The algorithm terminates when OPEN is empty.

Target

\text{OPEN} = \varnothing \implies \text{UPPER} = \operatorname{dist}(s, t) \in \overline{\mathbb{R}},

for every execution, under the nonnegative arc length assumption of §2.3 ( $a_{ij} \ge 0$ for every arc) — BertsekasDP.label_correcting_correctness_of_nonneg_arcs (goal). Milestones: termination — no infinite execution exists, which needs only the weaker nonnegative-cycle assumption (label_correcting_terminates) — and the workhorse invariant that every finite label is the length of an actual walk from $s$ , which needs neither (label_correcting_invariant).

The nonnegative-arc hypothesis is essential and not a formalization artifact: the algorithm prunes with the test $d_i + a_{ij} < \min\{d_j, \mathrm{UPPER}\}$ , and with a negative arc a longer prefix can still reach $t$ more cheaply, so the pruned node is never entered into OPEN. An earlier version of this mission's goal carried only the nonnegative-cycle assumption of §2.1 and was disproved by the counterexample $s=0$ , $t=2$ , $a_{02}=1$ , $a_{01}=2$ , $a_{12}=-2$ (a graph with no cycles at all), where the algorithm terminates with $\mathrm{UPPER}=1$ while the shortest distance is $0$ . Exercise 2.7 of the source treats the nonnegative-cycle case, which requires a modified algorithm.

Significance

Prop. 2.3.1 certifies simultaneously breadth-first search, Dijkstra (best-first), depth-first and small-label-first variants — every removal discipline is one refinement of the nondeterministic relation. Formally, the development contributes a reusable small-step framework for label-setting/correcting algorithms on which sharper results (Dijkstra's single-pass property, A* admissibility, §2.3.3) can later be built. The result is classical; the formal content is the induction along the nondeterministic step relation.

Difficulty

Termination is the subtle half: labels do not decrease monotonically along the run in an obvious well-founded way; the book's argument counts the finitely many distinct walk lengths below a bound — this needs the nonnegative-cycle assumption and a careful bound relating labels to simple-path lengths. The invariant proof must thread through the fold over children within a single step.

Formalization scope

Finite node type with decidable equality; arcs as a Finset of ordered pairs; lengths total on $V \times V$ (only arc values matter). The step relation is fully nondeterministic in pivot choice and child order (a permutation quantifier); correctness quantifies over all reachable terminal states — there is no fixed schedule to exploit. Distances live in EReal, so the no-path case is the honest empty infimum, not a sentinel. The trivializing risk of restricting to nonnegative arcs is avoided: only cycles are constrained.

Selected references

D. P. Bertsekas, Dynamic Programming and Optimal Control, Vol. I, 3rd ed., Athena Scientific, 2005. (Prop. 2.3.1, §2.3.) http://www.athenasc.com/dpbook.html
E. W. Dijkstra, A note on two problems in connexion with graphs, Numer. Math. 1 (1959), 269–271. https://doi.org/10.1007/BF01386390
R. Bellman, On a routing problem, Quart. Appl. Math. 16 (1958), 87–90. https://doi.org/10.1090/qam/102435

6 thms4 active users

Completed

Combinatorics·Captain: marwahaha

Sands–Sauer–Woodrow: monochromatic paths in two-coloured tournamentsResearch Paper

Motivation

A tournament is a directed graph in which every two distinct vertices are joined by exactly one arc — the model of a round-robin competition, and the setting of Ramsey theory's oldest questions.

In 1982 Sands, Sauer and Woodrow asked: if the arcs of a tournament are coloured with two colours, must some vertex be reachable from every other vertex along a monochromatic path, one whose arcs all carry the same colour? They answered yes [SSW82, Corollary 2, p. 273], through a theorem on arbitrary digraphs [SSW82, Theorem 1, pp. 271–273]. That theorem is also the two-colour case of kernel theory: kernels are independent dominating sets, they exist in digraphs whose arcs split into two transitive classes, and the stable-marriage theorem is a special case [Ch26, §1].

The tournament statement is the settled case of a question of Erdős that remains open: with three colours, must either a rainbow directed triangle occur, or a vertex reach every other vertex monochromatically [SSW82, PROBLEM, p. 275]? The platform already carries that open problem as the mission "Monochromatic reachability or rainbow triangles" (OPG1808.root_problem). This mission is the two-colour theory beside it, not a duplicate: it collects the results that are known and that any attack on the three-colour question builds on.

Timeline. Sands–Sauer–Woodrow (1982) prove Theorem 1, deduce the two-colour tournament statement, exhibit a three-coloured tournament with no vertex reaching all others, and ask whether three colours force a rainbow triangle or such a vertex [SSW82]. Shen Minggang (1988) proves the theorem for any number of colours when no triangle carries three distinct colours [Mi88]. Galeana-Sánchez and Rojas-Monroy (2005) give a six-vertex four-coloured tournament with neither, so three colours is the last case of the rainbow formulation [GR05]. Bousquet, Lochet and Thomassé (2017) show that a k-coloured tournament has a dominating set of size $O(\ln 2k \cdot k^{k+2})$ built from monochromatic paths — bounded, but not the single vertex of the two-colour case [BLT17]. Chancelier (2026) gives the first machine-checked proof of the general theorem, in Rocq, and records that no Lean formalization exists [Ch26].

Setting

Fix a vertex type $V$ . A digraph is a relation $D : V \to V \to \mathrm{Prop}$ , written $x \to y$ ; an arc colouring assigns each ordered pair a colour in $\mathrm{Fin}\,3$ ; a colouring uses at most two colours when every arc has colour $0$ or colour $1$ . A tournament is a loopless digraph in which every two distinct vertices are joined by exactly one arc.

A monochromatic path from $x$ to $y$ has distinct vertices, consecutive ones joined by an arc, all those arcs of one colour; write $x \rightsquigarrow y$ when one exists, and say that $x$ monochromatically reaches $y$ . A set $S$ is monochromatically independent when no two distinct members are connected by a monochromatic path in either direction — this is not graph independence: in a tournament a single arc joins any two vertices, so such a set has at most one element. A digraph has no monochromatic infinite outward path when no injective $x : \mathbb{N} \to V$ has all arcs $x_n \to x_{n+1}$ of one colour.

Formalization targets

Goal — the two-coloured tournament theorem (SSW Corollary 2)

$D$ a tournament on a nonempty finite vertex type, its arcs coloured with at most two colours:

\exists v,\ \forall x,\ x \neq v \Rightarrow x \rightsquigarrow v .

Milestone — the two-coloured digraph theorem (SSW Theorem 1)

$D$ any digraph on any vertex type, arcs coloured with at most two colours, with no monochromatic infinite outward path:

\exists S,\ S \text{ monochromatically independent} \ \wedge\ \forall x,\ x \notin S \Rightarrow \exists s \in S,\ x \rightsquigarrow s .

Milestone — the source form of the goal

The goal in the orientation of the platform's existing definition, the distinguished vertex reaching the others:

\exists s,\ \forall t,\ s \rightsquigarrow t .

Milestone — the blocked three-coloured theorem (SSW Theorem 3)

$T$ a tournament whose arcs carry three colours and whose vertices are partitioned into blocks, two vertices of different blocks always joined by a red arc and two of the same block by a blue or a green arc; then some vertex is monochromatically reached by every other.

Significance

The result. The goal settles the two-colour case of Erdős's question in the sharp form that one vertex suffices, and it is the base of the known theory: the paper's own block-coloured three-colour theorem is proved from it by iteration, and the kernel and stable-matching corollaries of the general theorem make it standard digraph theory. Without it the three-colour question has no settled case to compare against.

Formalizing it. No Lean formalization of these statements is recorded, for the corollary or for the general theorem [Ch26]; the machine-checked development that exists is in Rocq, for the general theorem, and is the first for the infinite case. This mission produces, in Lean, a classical theorem the platform does not have, together with the definitions it rests on: monochromatic reachability and monochromatic independence over an arbitrary vertex type. Status is stated per target: the goal is a theorem of the source paper, not an open question; the three-colour problem beside it remains open.

Difficulty

The first idea — take a longest monochromatic path and read off its end — does not close the argument. It gives monochromatic reachability only for the vertices on the path; for a vertex outside it, one knows only that the arcs from the path to that vertex cannot continue the path's colour, which yields no path back to the path's end. The source instead takes a maximal element, under a relation mixing the two colours, of a family of monochromatically independent sets — $S \preceq T$ when every $s \in S$ has $s \in T$ , or a blue path to some $t \in T$ with no red path back — and shows by a minimal-counterexample argument on red reachability that a maximal element is the required set. Over an arbitrary vertex type the family needs Zorn's lemma, and the no-infinite-outward-path hypothesis, not finiteness, is what bounds the argument. A second trap is definitional: because independence here is monochromatic, the tournament case collapses to one vertex; a formalization using graph independence would state a different and false theorem.

Formalization scope

Reuses the platform module opg1808_colored_tournaments: Digraph V := V → V → Prop, ArcColoring V := V → V → Fin 3, IsTournament, and MonochromaticallyReaches, the reflexive-transitive closure of one colour's arcs. A new definition supplies monochromatic independence; prose and statements use the same notation.
Colours are three-valued even when two occur, matching that module; the two-colour hypothesis says every arc has colour $0$ or colour $1$ . Relabelling two used colours into $\{0,1\}$ preserves which paths are monochromatic, so nothing is lost.
The source allows loops and multiple edges; the formalization uses a simple relation. Multiple edges are irrelevant, since reachability depends only on the presence of an arc, and loops are excluded by IsTournament. For the general digraph target loops change nothing, as the source's paths have distinct vertices.
The source's paths have distinct vertices while MonochromaticallyReaches uses walks; the two agree for reachability, and independence is stated through walks, so no distinctness hypothesis is needed.
The goal is stated on [Fintype V] [Nonempty V]; nonemptiness is required, the target being false on an empty vertex type. The general target is stated on an arbitrary type, and its hypothesis is vacuous in the finite case, which is the entry point for the goal.
The platform's IsMonochromaticSource is the reversed orientation of the goal; the goal follows the source paper, which orients paths towards the distinguished vertex.

Needed: the reused module, a definition of monochromatic independence, reachability lemmas for two colour classes, and for the general target Zorn's lemma and infinite outward paths. The reachability and independence layer is reusable by any later mission on coloured digraphs, including the three-colour problem beside this one. Contributions to any target are welcome.

Selected references

B. Sands, N. Sauer, R. Woodrow, On monochromatic paths in edge-coloured digraphs, J. Combin. Theory Ser. B 33 (1982), no. 3, 271–275. Theorem 1 (pp. 271–273), Corollary 2 (p. 273), Theorem 3 (pp. 274–275), PROBLEM (p. 275). https://doi.org/10.1016/0095-8956(82)90047-8
S. Minggang, On monochromatic paths in m-coloured tournaments, J. Combin. Theory Ser. B 45 (1988), 108–111. https://doi.org/10.1016/0095-8956(88)90062-2
H. Galeana-Sánchez, R. Rojas-Monroy, Monochromatic paths and at most 2-colored arc sets in edge-coloured tournaments, Graphs Combin. 21 (2005), 307–317. https://doi.org/10.1007/s00373-005-0627-y
M. Melcher, K. B. Reid, Monochromatic sinks in nearly transitive arc-colored tournaments, Discrete Math. 310 (2010), 2697–2704. https://doi.org/10.1016/j.disc.2010.05.017
N. Bousquet, W. Lochet, S. Thomassé, A proof of the Erdős–Sands–Sauer–Woodrow conjecture, arXiv:1703.08123 (2017). https://arxiv.org/abs/1703.08123
J.-P. Chancelier, A formal proof of the Sands-Sauer-Woodrow theorem using the Rocq prover and mathcomp/ssreflect, arXiv:2604.21376 (2026). https://arxiv.org/abs/2604.21376
Open Problem Garden, Monochromatic reachability or rainbow triangles. https://www.openproblemgarden.org/op/monochromatic_reachability_vs_rainbow_triangles

6 thms3 active usersReviewed

Information Theory Quantum Error Correction·Captain: mikedeng1

Quantum Expander Codes: On a Biregular Left-Right Expanding Graph with δA, δB < 1/6, the Greedy Generator Decoder Corrects Every Quantum Error of Weight Below min(γA·nA, γB·nB)/(3(1+ΔB))Research Paper

Motivation

A quantum LDPC code is a CSS code whose two check matrices $H_X$ and $H_Z$ have rows and columns of bounded weight, so that every check measures only a few qubits. Such codes are the main candidates for fault-tolerant quantum memories, because their checks are local, but a code is only useful together with a decoder: an efficient procedure that recovers the error, up to stabilizers, from its syndrome. For classical LDPC codes built from expander graphs, Sipser and Spielman showed in 1996 that a simple bit-flipping algorithm corrects a constant fraction of the minimum distance in linear time (Sipser–Spielman 1996). In the quantum setting the obvious analogue fails, and before this work no family of quantum LDPC codes was known to admit an efficient decoder correcting a number of adversarial errors proportional to its minimum distance.

Timeline.

1996: Sipser and Spielman, expander codes and their linear-time bit-flipping decoder.
2009: Tillich and Zémor introduce the hypergraph product, giving quantum LDPC codes of positive rate and minimum distance of order $\sqrt n$ (arXiv:0903.0566).
2015: Leverrier, Tillich and Zémor take the hypergraph product of an expanding biregular graph with itself and prove that a greedy generator-flipping decoder corrects every error of weight up to a constant fraction of the minimum distance (arXiv:1504.00822, FOCS 2015). This mission formalizes that result.

Setting

Let $G = (A \cup B, \mathcal E)$ be a finite bipartite graph, $n_A = |A|$ , $n_B = |B|$ , with $n_B \le n_A$ , and write $a \sim b$ for adjacency. $G$ is $(\Delta_A, \Delta_B)$ -biregular if every vertex of $A$ has $\Delta_A$ neighbours and every vertex of $B$ has $\Delta_B$ . For $S \subseteq A$ let $\Gamma(S)$ be its neighbourhood. $G$ is $(\gamma_A, \delta_A)$ -left-expanding if $|\Gamma(S)| \ge (1 - \delta_A)\Delta_A |S|$ for every $S \subseteq A$ with $|S| \le \gamma_A n_A$ ; right expansion is the same on the $B$ side, and left-right expanding means both. $\Gamma_u(S)$ denotes the unique neighbours of $S$ , adjacent to exactly one vertex of $S$ .

Let $H$ be the $n_B \times n_A$ binary biadjacency matrix of $G$ . The quantum code $\mathcal Q_G$ has $n = n_A^2 + n_B^2$ qubits, indexed by $A^2 \cup B^2$ (written $\alpha a$ and $b\beta$ ), and check matrices

H_X = (\mathbb 1_{n_A} \otimes H,\ H^T \otimes \mathbb 1_{n_B}), \qquad H_Z = (H \otimes \mathbb 1_{n_A},\ \mathbb 1_{n_B} \otimes H^T),

with rows indexed by $A \times B$ and $B \times A$ . The row $ba$ of $H_Z$ has support the Z-generator $g_{ba} = \{\alpha a : \alpha \sim b\} \cup \{b\beta : \beta \sim a\}$ . An $X$ error is $e \in \mathbb F_2^{A^2 \cup B^2}$ , its syndrome is $\sigma_X(e) = H_X e^T$ , and $\mathcal C_Z^\perp$ is the space of sums of Z-generators. The weight $w(e_X, e_Z)$ of a quantum error counts the qubits where $e_X$ or $e_Z$ is nonzero.

The decoder. On a syndrome $s$ , one iteration picks a vector $e_1$ whose support lies in some generator $g_{ba}$ , such that $s_1 = s + \sigma_X(e_1)$ has $|s_1| < |s|$ and the ratio $(|s| - |s_1|)/|e_1|$ is maximal among all such vectors. It iterates on the current syndrome, fails if it gets stuck at a nonzero syndrome, and otherwise outputs the sum $e_O$ of the flipped vectors. The $Z$ decoder is the same with $H_X$ and $H_Z$ exchanged.

Formalization targets

Goal: Theorem 2

Assume $G$ is $(\Delta_A, \Delta_B)$ -biregular and $(\gamma_A, \delta_A, \gamma_B, \delta_B)$ -left-right expanding with

\delta_A < \tfrac16, \qquad \delta_B < \tfrac16,

and let $(e_X, e_Z)$ be a quantum error with

w(e_X, e_Z) < w_0 = \frac{1}{3(1 + \Delta_B)} \min(\gamma_A n_A, \gamma_B n_B).

Then on every run, the $X$ decoder on input $\sigma_X(e_X)$ never outputs a failure and its output satisfies $e_O + e_X \in \mathcal C_Z^\perp$ . The $Z$ decoder on $\sigma_Z(e_Z)$ behaves symmetrically, with $e_O + e_Z \in \mathcal C_X^\perp$ .

Milestones

In the paper's order of proof:

Lemma 3, $|\Gamma_u(S_A)| \ge (1 - 2\delta_A)\Delta_A |S_A|$ ;
Proposition 4, distance at least $\gamma_A n_A$ for the classical code;
the distance half of eq. (3), $d_Q \ge \min(d, d^T)$ , already posed on the platform;
Corollary 5, $d_Q \ge \min(\gamma_A n_A, \gamma_B n_B)$ ;
the column-weight bound $|\sigma_X(e)| \le \Delta_B |e|$ ;
Lemma 7, existence of a critical generator;
the displays (19), (22), (23), (24) of Appendix B;
Lemma 8, a step of ratio at least $1/3$ inside a critical generator;
Lemma 10, the $X$ half of the goal.

Significance

The result. Theorem 2 gives the first family of quantum LDPC codes with an efficient decoder that corrects a number of adversarial errors proportional to the minimum distance. Here that number is of order $\sqrt n$ . The same analysis yields a robustness property: low-weight errors have syndromes of proportional weight (Corollary 9 of the paper). Later work on quantum expander codes builds on this analysis, for example on their decoding under random noise (arXiv:1711.08351) and on fault tolerance with constant overhead (arXiv:1808.03821).

Formalizing it. The result is proved on paper. As far as is known, it has no machine-checked proof. The mission produces a formal statement of the decoder and its correctness, and it also produces reusable pieces:

unique-neighbour expansion;
the distance of expander codes;
the distance of hypergraph product codes, tied to an open item of the Tillich–Zémor mission;
a generic formalization of greedy syndrome-weight decoding.

Difficulty

The obvious quantum analogue of Sipser–Spielman flips single qubits that lower the syndrome weight. It fails because of degeneracy: an error and its sum with a generator have the same syndrome. A small error can therefore look locally like a large one, and no single qubit need be worth flipping. The paper's decoder instead flips arbitrary patterns inside one generator. The difficulty is to show that some pattern always lowers the syndrome weight by a constant fraction of its size. The proof needs a combinatorial structure, the critical generator, whose existence uses unique-neighbour expansion on both sides of the graph, and a case analysis on its six parts. A second difficulty is that the decoder minimizes the syndrome weight, not the error weight, so the intermediate error can grow. Bounding that growth is what limits the guarantee to $w_0$ rather than the distance.

Formalization scope

The graph is a relation adj : A → B → Prop on finite types, and $H$ = bipMatrix adj : Matrix B A (ZMod 2).
The published TillichZemor.HGP.Setting is reused. The paper's $H_X$ is TillichZemor.HGP.hz H H and its $H_Z$ is hx H H; the X/Z names are swapped relative to the 2009 paper, and this is checked against eq. (5) in a sanity file.
Qubits are (A × A) ⊕ (B × B), weights are hammingNorm, and $\mathcal C_Z^\perp$ is CodingTheory.dualCode of ker H_Z.
Expansion constants are real and cardinalities are compared in $\mathbb R$ . Distance statements are per-vector, so no $\infty$ -valued minimum distance is cast to a real number.
The decoder is defined once (Candidate, Step, Reach, DecodesCorrectly), generic in the syndrome and generator matrices. Its ratio is computed in $\mathbb Q$ .
Reach contains every state reachable under any tie-breaking. Correctness requires, at every reachable state, a further step while the syndrome is nonzero, and $e_O + e$ in the row space of the generator matrix once it is zero. Termination is automatic, because each step lowers a natural number.

Additions and omissions.

The hypothesis $\Delta_A \ge 1$ is added throughout. With $\Delta_A = 0$ the expansion conditions are vacuous, $H = 0$ , and every error is invisible.
In Lemma 8 the vector $e_1$ is required to be nonzero. With $e_1 = 0$ the printed inequality reads $0 \ge 0$ .
Lemma 8 is posed in its first assertion only. The critical generator is taken with respect to a minimum-weight representative of the coset, as in Appendix B.
The clauses "runs in time linear in the code length" and "letting $\Delta_A$ , $\Delta_B$ be fixed and allowing $n_A, n_B$ to grow" are not formalized. The goal holds for every finite graph meeting the hypotheses.

Trivializing formalizations ruled out. The goal names the paper's own decoder, not "there exists a decoder", which a brute-force coset decoder would satisfy. It quantifies over every run, not a single favourable one. It asserts both never-failing and correctness, not partial correctness alone. It uses $H_X$ = hz H H, not the swapped matrix.

Welcome contributions. Proofs of the counting milestones (Lemma 3, Proposition 4, the column-weight bound, (19), (22)–(24)) are independent of one another. The distance bound of Tillich–Zémor, open on the platform, is the deepest dependency. Unique-neighbour expansion and the hypergraph-product distance bound are useful beyond this mission.

Selected references

A. Leverrier, J.-P. Tillich, G. Zémor, Quantum expander codes, FOCS 2015; arXiv:1504.00822v1 (2015). https://arxiv.org/abs/1504.00822
J.-P. Tillich, G. Zémor, Quantum LDPC codes with positive rate and minimum distance proportional to the square root of the blocklength, IEEE Trans. Inf. Theory 60(2), 2014; arXiv:0903.0566. https://arxiv.org/abs/0903.0566
M. Sipser, D. A. Spielman, Expander codes, IEEE Trans. Inf. Theory 42(6), 1996. https://doi.org/10.1109/18.556667
O. Fawzi, A. Grospellier, A. Leverrier, Efficient decoding of random errors for quantum expander codes, STOC 2018; arXiv:1711.08351. https://arxiv.org/abs/1711.08351
O. Fawzi, A. Grospellier, A. Leverrier, Constant overhead quantum fault-tolerance with quantum expander codes, FOCS 2018; arXiv:1808.03821. https://arxiv.org/abs/1808.03821

16 thms3 active usersReviewed

Combinatorics·Captain: mikedeng1

A Solution to the 1-2-3 Conjecture: Every Finite Graph Without a K2 Component Has an Edge-Weighting from {1,2,3} Whose Weighted Degrees Properly Color the VerticesResearch Paper

Motivation

Many graph-colouring questions ask whether a proper colouring can be produced indirectly, from local data, instead of being assigned vertex by vertex. In the 1-2-3 Conjecture, the colours are produced by weighting the edges of a graph and colouring each vertex with the sum of the weights at it. Karoński, Łuczak and Thomason asked in 2004 whether weights from $\{1,2,3\}$ always suffice (J. Combin. Theory Ser. B 91 (2004)). The question started as a local version of the irregularity strength problem, where all vertices, not only adjacent ones, must receive different sums. It became one of the most studied problems on graph labellings. Surveys: Seamone (arXiv:1211.5122) and Grytczuk (DOI 10.1016/j.ejc.2020.103213).

Timeline.

2004: Karoński, Łuczak, Thomason state the conjecture and prove it for 3-colourable graphs.
2007: Addario-Berry, Dalal, McDiarmid, Reed and Thomason give the first finite bound, $k=30$ ; later $k=16$ (Addario-Berry et al.) and $k=13$ (Wang and Yu).
2010: Kalkowski, Karoński and Pfender reach $k=5$ (J. Combin. Theory Ser. B 100 (2010)).
Before 2023: Przybyło proves the conjecture for $d$ -regular graphs with $d\ge 10^8$ and for graphs with minimum degree $\delta(G)\ge C\log\Delta(G)$ ; Zhong proves it for graphs with minimum degree at least $0.99985|V|$ (references [20], [21], [31] of the paper).
2023: Keusch reaches $k=4$ with a maximum-cut and flow argument (Combinatorica 43 (2023), 651–658; reference [18] of the paper).
2024: Keusch proves the conjecture, $k=3$ (J. Combin. Theory Ser. B (2024), arXiv:2303.02611).

Setting

Let $G=(V,E)$ be a finite simple graph and write $N(v)$ for the neighbourhood of a vertex $v$ . A $k$ -edge-weighting is a function $\omega:E\to\{1,\dots,k\}$ . The weighted degree of $v$ is

s_\omega(v)=\sum_{w\in N(v)}\omega(\{v,w\}).

Two adjacent vertices $v,w$ have a coloring conflict if $s_\omega(v)=s_\omega(w)$ . The weighting is vertex-coloring if no edge is a coloring conflict, that is, if $s_\omega$ is a proper vertex colouring of $G$ .

If $G$ has a connected component consisting of a single edge $\{v,w\}$ (a component isomorphic to $K_2$ ), then $s_\omega(v)=s_\omega(w)=\omega(\{v,w\})$ for every $\omega$ , so no weighting is vertex-coloring. This is the only obstruction.

The proof uses a few further objects:

for $W\subseteq V$ , $\deg_W(v)=|N(v)\cap W|$ ;
for disjoint $S,T\subseteq V$ , the bipartite subgraph $G(S,T)$ with vertex set $S\cup T$ and the edges of $G$ between $S$ and $T$ ;
a good R-B-partition (Definition 6): a partition $V=R\cup B$ with $R$ independent, $G(R,B)$ connected and $|B|$ even;
a maximum cut $C=(S,T)$ and an auxiliary unit-capacity flow network $G_{C,F,\sigma}$ built from it (Lemma 4).

The Lean names are wdeg G ω v for $s_\omega(v)$ , IsWeighting G k ω, IsVertexColoring G ω, NoK2Component G and IsGoodPartition G U R B.

Formalization targets

Goal: Theorem 1 (p. 2)

If no connected component of $G$ is isomorphic to $K_2$ , then there is $\omega:E\to\{1,2,3\}$ with

\sum_{u\in N(v)}\omega(\{u,v\})\ne\sum_{u\in N(w)}\omega(\{u,w\})\qquad\text{for every edge }\{v,w\}\in E.

The connected case (p. 14)

Every finite connected graph with $|V|\ge 3$ has a vertex-coloring $\{1,2,3\}$ -edge-weighting. This is the statement the case analysis of the proof establishes. Theorem 1 follows by treating each component separately.

Milestones along the proof

In the order the proof uses them:

Lemma 2: an independent set $R$ with $G(R,V\setminus R)$ connected, alternating along a shortest path.
Lemma 4: a flow of value $|F|$ in $G_{C,F,\sigma}$ .
Lemma 3: a weighting and odd designated colours $f$ , proper on $G$ , with $|s_\omega+h-f|=1$ .
Lemma 5: a bipartite weighting with prescribed parities on $R$ and exact weighted degrees on $B$ , plus a second version with extra control along a fixed path.
Lemmas 7, 8 and 9: the three basic situations in which a good R-B-partition of $G$ , or of $G$ minus one vertex, yields a vertex-coloring weighting.
Lemma 10: every connected graph of minimum degree at least $2$ has an edge whose removal, together with its two ends, leaves a connected graph.

Significance

The result. Theorem 1 settles a conjecture that was open for nineteen years. The constant is optimal: the triangle $K_3$ has no vertex-coloring $\{1,2\}$ -weighting (two of its three edges get the same weight, and then two vertices tie), and deciding whether a vertex-coloring $\{1,2\}$ -weighting exists is NP-complete (Dudek and Wajc, 2011). Theorem 1 also closes the sequence of upper bounds $30,16,13,6,5,4$ on the number of weights needed. Variants remain open: total weightings with vertex weights $\{1,2\}$ and edge weights $\{1,2\}$ (the 1-2 Conjecture), and list versions.

Formalizing it. The theorem is proved, in a 16-page paper. As far as is known it has no machine-checked proof. A formal proof would verify the case analysis at the end of the paper (pp. 11–14, about fifteen sub-cases with three auxiliary graphs), which is where errors in such arguments usually hide. The flow lemma is quoted from the 2023 paper and not reproved here. Formalizing it means proving an integral max-flow statement for a specific unit-capacity network, and the result can be reused for other flow-based weighting arguments.

Difficulty

The obvious approach is to fix the weights greedily, edge by edge or vertex by vertex. This fails because changing one edge weight changes two weighted degrees at once, so a repair at one vertex can create a conflict at a neighbour. With only three weights there is no room to absorb this. Every earlier bound above $3$ used the extra weight as slack.

The difficulty in the paper is parity. The construction needs the set $B$ of blue vertices to have even cardinality, and $|B|$ cannot always be made even. The proof therefore removes one or two vertices, applies one of three base lemmas, and re-inserts the vertices. That re-insertion may need one more round of weight changes along a path. Each sub-case has to keep track of parities, of exact weighted degrees on $B$ , and of the connectivity of $G(R,B)$ simultaneously.

Formalization scope

Representation.

Graphs are SimpleGraph V on a finite vertex type V with decidable adjacency. The paper's "graph" is a finite simple graph: weighted degrees are finite sums, and the proof uses a maximum cut and vertex orderings.
An edge-weighting is a function ω : Sym2 V → ℕ on unordered pairs. IsWeighting G k ω requires $\omega(e)\in\{1,\dots,k\}$ for every edge $e$ of $G$ ; values on non-edges are unconstrained and never used.
The weighted degree sums over G.neighborFinset v. Since $\{u,v\}=\{v,u\}$ in Sym2, the single sum equals both sides of Theorem 1's displayed inequality.
"No component isomorphic to $K_2$ " uses Mathlib's connected components and graph isomorphism. A sanity file proves it equivalent to "no edge both of whose ends have degree 1".
$G(R,B)$ is Mathlib's G.between R B, induced on $R\cup B$ wherever that vertex set is not all of $V$ .

Conventions that differ from the page. There are two, both disclosed in the item statements:

The vertex type is finite.
The flow of Lemma 4 is integral. The page says "an $s$ - $t$ -flow"; the paper uses integrality immediately afterwards, and the two versions are equivalent by the integrality theorem.

Lemma 5's condition $\alpha(v)\in\{2\deg(v)-1,2\deg(v),2\deg(v)+1\}$ is stated in $\mathbb Z$ , and Lemma 3's $|s_\omega+h-f|=1$ is computed in $\mathbb Z$ .

Ruled out. None of the following formalizations is faithful:

weights allowed to be $0$ , which deletes edges;
weights constrained off the edges;
the $K_2$ hypothesis strengthened to minimum degree at least $2$ , or to connectivity;
"adjacent vertices" replaced by "all pairs of vertices", which is the irregularity-strength problem.

Infrastructure. A complete development needs:

spanning trees and parity arguments on trees (Lemma 5);
depth-first search trees (Lemma 10);
maximum cuts and an integral max-flow or augmenting-path argument for $G_{C,F,\sigma}$ (Lemma 4), together with path decompositions of unit flows (the proof of Lemma 3).

The flow and cut definitions are stated for arbitrary finite graphs and can be reused. Contributions are welcome at every level: proofs of individual lemmas, general flow-decomposition results, and the final case analysis.

Selected references

R. Keusch, A Solution to the 1-2-3 Conjecture, J. Combin. Theory Ser. B, 2024. arXiv:2303.02611v4, DOI 10.1016/j.jctb.2024.01.002
R. Keusch, Vertex-coloring graphs with 4-edge-weightings, Combinatorica 43 (2023), 651–658. Cited as [18] in arXiv:2303.02611v4.
M. Karoński, T. Łuczak, A. Thomason, Edge weights and vertex colours, J. Combin. Theory Ser. B 91 (2004), 151–157. DOI 10.1016/j.jctb.2003.12.001
M. Kalkowski, M. Karoński, F. Pfender, Vertex-coloring edge-weightings: towards the 1-2-3-conjecture, J. Combin. Theory Ser. B 100 (2010). DOI 10.1016/j.jctb.2009.06.002
A. Dudek, D. Wajc, On the complexity of vertex-coloring edge-weightings, Discrete Math. Theor. Comput. Sci. 13 (2011), 45–50. Cited as [11] in arXiv:2303.02611v4.
B. Seamone, The 1-2-3 Conjecture and related problems: a survey, 2012. arXiv:1211.5122
J. Grytczuk, From the 1-2-3 Conjecture to the Riemann Hypothesis, European J. Combin. 91 (2021), 103213. DOI 10.1016/j.ejc.2020.103213

14 thms3 active usersReviewed

Combinatorics·Captain: mikedeng1

Generalized Turán Problems for Even Cycles 6: The Maximum Number of (2l+1)-Cycles in a Graph with No Cycle of Length 3, …, 2l or 2k+1 Is Ω(n^{1+1/(2k+2)}) and O(n²)Research Paper

Motivation

Generalized Turán problems ask for the maximum number of copies of a fixed graph $H$ in an $n$ -vertex graph that avoids a family $\mathcal F$ of forbidden subgraphs. The ordinary Turán number counts edges ( $H = K_2$ ); Alon and Shikhelman (arXiv:1506.03397) started the systematic study of the general function $\mathrm{ex}(n, H, \mathcal F)$ , building on earlier results of Erdős on cliques, Bollobás and Győri on pentagons in triangle-free graphs, and Győri and Li on triangles in graphs without a long odd or even cycle. Counting cycles in graphs with forbidden cycles is closely tied to extremal problems for Berge hypergraphs, and the constructions used are sparse hypergraphs of large girth.

Gerbner, Győri, Methuku and Vizer, Generalized Turán problems for even cycles (arXiv:1712.07079, J. Combin. Theory Ser. B, 2020), determine or bound $\mathrm{ex}(n, C_{\ell}, \mathcal F)$ for many cycle families. This mission covers one of their results in §6.2: the number of odd cycles $C_{2l+1}$ in a graph in which every shorter cycle is forbidden and, in addition, one longer odd cycle $C_{2k+1}$ is forbidden. Its companion (Theorem 17, a separate mission of this series) forbids a longer even cycle $C_{2k}$ instead, and there the paper obtains a sub-quadratic upper bound; with an odd extra cycle only a quadratic upper bound is proved.

Setting

All graphs are finite and simple. For an integer $a \ge 3$ , $C_a$ is the cycle of length $a$ . For a set $A$ of integers $a \ge 3$ , write $\mathcal C_A = \{C_a : a \in A\}$ ; a graph is $\mathcal C_A$ -free if it contains no $C_a$ with $a \in A$ as a (not necessarily induced) subgraph. The family $\mathcal C_{2l}$ consists of all cycles $C_3, C_4, \dots, C_{2l}$ .

For graphs $H$ and $G$ , $\mathcal N(H, G)$ is the number of copies of $H$ in $G$ : subgraphs of $G$ isomorphic to $H$ , counted without labelling. The generalized Turán number is

\mathrm{ex}(n, H, \mathcal F) = \max\{\mathcal N(H, G) : G \text{ has } n \text{ vertices and contains no member of } \mathcal F\}.

For a vertex $v$ of $G$ , $N_i(v)$ is the set of vertices at distance exactly $i$ from $v$ .

A hypergraph is a finite set of hyperedges (vertex sets); it is $r$ -uniform if each hyperedge has $r$ vertices. A Berge cycle of length $j \ge 2$ is a sequence $v_1, h_1, v_2, h_2, \dots, v_j, h_j, v_1$ of distinct vertices and distinct hyperedges with $v_i, v_{i+1} \in h_i$ and $v_j, v_1 \in h_j$ . The girth of a hypergraph is the length of its shortest Berge cycle; "girth at least $s$ " means there is no Berge cycle of length $2, \dots, s-1$ .

Formalization targets

Goal: Theorem 18

For all integers $k > l \ge 2$ , as $n \to \infty$ ,

\Omega\big(n^{1+\frac{1}{2k+2}}\big) = \mathrm{ex}\big(n, C_{2l+1}, \mathcal C_{2l} \cup \{C_{2k+1}\}\big) = O(n^2).

Both the lower and the upper bound are part of the goal; the implied constants may depend on $k$ and $l$ only.

Milestones

Theorem 29 (Nešetřil–Rödl). For $r \ge 2$ , $s \ge 3$ and all large $n$ there is an $r$ -uniform hypergraph on $n$ vertices of girth at least $s$ with at least $n^{1+1/s}$ hyperedges.
The construction. Replacing each hyperedge of a $(2l+1)$ -uniform hypergraph of girth at least $2k+2$ by a copy of $C_{2l+1}$ yields a graph with no cycle of length at most $2k+1$ other than $2l+1$ , and with at least as many copies of $C_{2l+1}$ as hyperedges.
Cycles through a vertex. In a $\mathcal C_{2l} \cup \{C_{2k+1}\}$ -free graph there is no edge inside $N_i(v)$ for $i < l$ , every $C_{2l+1}$ through $v$ uses exactly one edge inside $N_l(v)$ , and so the number of $C_{2l+1}$ 's through $v$ is at most the number of edges inside $N_l(v)$ .
Claim 19. In a $\mathcal C_{2l} \cup \{C_{2k+1}\}$ -free graph the number of edges inside $N_l(v)$ is at most $C(k,l)\,|N_l(v)| \le C(k,l)\, n$ .

The supporting published theorem erdos_gallai_path_conjecture (the Erdős–Gallai path theorem: a graph on $n$ vertices with no path of $m+1$ edges has at most $mn/2$ edges) is included as a reference item; the paper's proof of Claim 19 invokes it.

Significance

Theorem 18 shows that forbidding all cycles up to length $2l$ together with one odd cycle $C_{2k+1}$ still permits polynomially more than $n$ copies of $C_{2l+1}$ , at least $n^{1 + 1/(2k+2)}$ , and at most $O(n^2)$ . Compared with Theorem 17, where an even cycle $C_{2k}$ is forbidden and the count is $O(n^{1+l/(l+1)})$ , it isolates the role of the parity of the extra forbidden cycle. The authors conjecture that the true order is sub-quadratic (Conjecture 34, §8 of the paper), so the gap between the two exponents in Theorem 18 is a stated open question; a formal development of the known bounds is the base on which any improvement would be checked.

The result is proved in the paper; to the best of current knowledge it has no machine-checked proof. Formalizing it produces: a reusable encoding of generalized Turán numbers for cycle families on top of Mathlib's copyCount; Berge cycles and the girth of uniform hypergraphs; distance layers $N_i(v)$ ; and a formal statement of the Nešetřil–Rödl existence theorem, which is used as a black box by many extremal constructions.

Difficulty

The upper bound requires careful bookkeeping of distance layers around a vertex in a graph without short cycles. The obvious estimate, bounding the copies of $C_{2l+1}$ through $v$ by the number of pairs of vertices of $N_l(v)$ , gives only $|N_l(v)|^2$ per vertex and hence nothing better than the trivial bound overall; the content of Claim 19 is that forbidding the single cycle $C_{2k+1}$ makes the edge count inside $N_l(v)$ linear, and the parity of $2k+1$ is used essentially.

The lower bound rests on Theorem 29, a cited result that is not proved in the paper, and for which Mathlib has no supporting theory of uniform hypergraphs or Berge cycles. For the construction itself, the paper only asserts that the cycle-replacement graph has no short cycle other than the inserted $C_{2l+1}$ 's; a cycle of the graph may wander through many hyperedges, and relating it to the girth of the hypergraph is the step a formal proof has to supply.

Formalization scope

Vertices of an $n$ -vertex graph are Fin n; graphs are SimpleGraph (Fin n). Cycles are Mathlib's SimpleGraph.cycleGraph, and $\mathcal N(H, G)$ is Mathlib's unlabelled copyCount.
$\mathcal C_{2l} \cup \{C_{2k+1}\}$ is encoded as the set of lengths Set.Icc 3 (2 * l) ∪ {2 * k + 1}: every length $3, \dots, 2l$ , not only $2l$ .
$\mathrm{ex}(n, H, \mathcal C_A)$ is the supremum of a nonempty finite set of natural numbers, hence a true maximum (checked in a sanity file).
$N_i(v)$ uses the extended distance edist, so vertices of other components lie in no layer.
Hypergraphs are Finset (Finset V); "girth at least $s$ " is a predicate (no Berge cycle of length $2, \dots, s-1$ ), not an infimum, so a hypergraph without Berge cycles has every girth.
$\Omega$ and $O$ are Mathlib's Asymptotics.IsBigO along atTop, with real exponents; both directions of the goal are stated.
Claim 19's $O(\cdot)$ is a single constant chosen before $n$ , the graph and the vertex. The milestone on cycles through $v$ uses the page's $\mathcal C_{2l} \cup \{C_{2k+1}\}$ -freeness assumption.

A formalization that states only the upper bound, uses labelled copies, lets a constant depend on the graph, omits the short cycles $C_3, \dots, C_{2l-1}$ from the forbidden family, or defines $\mathrm{ex}$ by a supremum that can take a junk value, does not prove this theorem.

Contributions welcome: proofs of the milestones, a proof of Theorem 29, and general lemmas on breadth-first layers in graphs of large girth, which are reusable by the companion missions of this series.

Selected references

D. Gerbner, E. Győri, A. Methuku, M. Vizer, Generalized Turán problems for even cycles, J. Combin. Theory Ser. B (2020); arXiv:1712.07079v3. https://arxiv.org/abs/1712.07079, https://doi.org/10.1016/j.jctb.2020.05.005
N. Alon, C. Shikhelman, Many T copies in H-free graphs, J. Combin. Theory Ser. B 121 (2016). https://arxiv.org/abs/1506.03397
J. Nešetřil, V. Rödl, On a probabilistic graph-theoretical method, Proc. Amer. Math. Soc. 72(2), 417–421 (1978). https://www.ams.org/journals/proc/1978-072-02/
P. Erdős, T. Gallai, On maximal paths and circuits of graphs, Acta Math. Acad. Sci. Hungar. 10 (1959). https://doi.org/10.1007/BF02024498

7 thms3 active usersReviewed

Completed

Combinatorics·Captain: mikedeng1

Twin-width I: Tractable FO Model Checking 1: Every Graph with Boolean-width k Has Twin-width at Most 2^(k+1) − 1Research Paper

Motivation

Twin-width was introduced by Bonnet, Kim, Thomassé and Watrigant (J. ACM 69(1), Article 3, 2021) as a graph parameter under which first-order model checking is fixed-parameter tractable when a contraction sequence is given. Its interest lies in the classes it covers at once: planar and, more generally, $K_t$ -minor-free graphs, bounded-degree grids, unit ball graphs of bounded clique number, and the classes of bounded rank-width or clique-width. These are the classical dense-graph width measures, for which FO (indeed MSO $_1$ ) model checking was already known to be tractable through Courcelle–Makowsky–Rotics.

This mission formalizes the link to the dense width measures, stated in the paper through boolean-width (Bui-Xuan, Telle and Vatshelle, Theor. Comput. Sci. 412(39), 2011). It is known that $\operatorname{boolw}(G)\le\operatorname{modw}(G)\le\operatorname{cw}(G)\le 2^{\operatorname{rw}(G)+1}-1$ (Vatshelle's PhD thesis, Chapter 4), so a bound on twin-width in terms of boolean-width shows that bounded twin-width captures bounded rank-width, clique-width, module-width and boolean-width simultaneously.

Setting

Let $G$ be a finite simple graph on a vertex set $V$ .

Two vertex sets $X,Y\subseteq V$ are homogeneous if either all pairs $(x,y)\in X\times Y$ are edges or none is. For a partition $\mathcal P$ of $V$ , a part $X$ has red degree equal to the number of other parts $Y\ne X$ that are not homogeneous to $X$ ; $\mathcal P$ is a $d$ -partition if every part has red degree at most $d$ . The graph $G$ has twin-width at most $d$ , written $\operatorname{tww}(G)\le d$ , if there are partitions $\mathcal P_0,\dots,\mathcal P_N$ of $V$ with $\mathcal P_0$ the partition into singletons, $\mathcal P_N$ having at most one part, each $\mathcal P_{i+1}$ obtained from $\mathcal P_i$ by merging two parts, and every $\mathcal P_i$ a $d$ -partition. This is the paper's partition form (p. 3:32) of its definition through trigraphs and red edges (pp. 3:11–3:12).

A decomposition tree of $G$ is a rooted binary tree $T$ , every internal node having exactly two children, whose leaves are in one-to-one correspondence with $V$ . Each edge $e$ of $T$ lies above exactly one rooted subtree and induces a cut $P_e=(A_e,B_e)$ of $V$ : $A_e$ is the set of leaf labels of that subtree and $B_e=V\setminus A_e$ . For disjoint $A,B$ write

\nu_G(A,B)=\bigl|\{N(S)\cap B: S\subseteq A\}\bigr|,

the number of different neighbourhoods in $B$ of subsets of $A$ , the empty subset included. The boolean-width of the cut is $\log_2\nu_G(A,B)$ , the boolean-width of $T$ is its maximum over the edges of $T$ , and $\operatorname{boolw}(G)$ is the minimum over all decomposition trees. In Lean, nbhdCount G A B is $\nu_G(A,B)$ , and BoolWidthLE G N states that some decomposition tree has $\nu_G(A_e,B_e)\le N$ on every edge, so $\operatorname{boolw}(G)\le k$ is BoolWidthLE G (2^k).

Formalization targets

Goal: Theorem 4.2 (p. 3:14)

Every graph with boolean-width $k$ has twin-width at most $2^{k+1}-1$ . With $N=2^{k}$ , the integer neighbourhood count,

\operatorname{BoolWidthLE}(G,N)\ \Longrightarrow\ \operatorname{tww}(G)\le 2N-1 .

Milestones (proof of Theorem 4.2, p. 3:14)

A graph with at most $N$ vertices has $\operatorname{tww}(G)\le N$ .
A rooted binary tree with more than $2N$ leaves ( $N\ge1$ ) has a rooted subtree below some edge with between $N+1$ and $2N$ leaves.
If $\nu_G(A,B)\le N$ and $|A|\ge N+1$ , two distinct vertices of $A$ have the same neighbourhood in $B$ .
If $(A,B)$ partitions $V$ , $|A|\le 2N$ , and $u\ne v\in A$ have the same neighbourhood in $B$ , then contracting $u$ and $v$ yields a $(2N-1)$ -partition.

Significance

The theorem places the classes of bounded boolean-width, and therefore of bounded clique-width and rank-width, inside the classes of bounded twin-width, with a single-exponential bound. Combined with the paper's model-checking algorithm, it recovers tractability of FO model checking on these classes once a contraction sequence is computed, and it situates twin-width as a common generalization of the dense width measures and of sparse classes such as $K_t$ -minor-free graphs.

No machine-checked version of twin-width or boolean-width is known to exist; neither notion is in Mathlib. The mission produces Lean definitions of twin-width in partition form, of decomposition trees and of the neighbourhood count behind boolean-width, together with the four combinatorial steps the paper's proof states explicitly. The definitions are shared, in identical form, with the other missions of this series on the same paper.

Difficulty

The first three milestones are elementary: a counting bound on contraction sequences, a walk down a binary tree, and a pigeonhole argument. The fourth is a direct count of non-homogeneous parts.

The difficulty is the iteration. After the first contraction the leaves of the updated tree are contracted vertices, so "the same neighbourhood in $B_e$ " must be read as homogeneity to all of $B_e$ for a set of vertices, and the boolean-width bound of the cuts must be re-established for sets rather than single vertices. The paper asserts the invariant that the contractions never create a red component of more than $2^{k+1}$ vertices without proving it. A complete proof of the goal therefore has to supply an invariant, carried through all $|V|-1$ contractions, that keeps every part's red degree below $2N-1$ . The naive repetition of the first step does not by itself control red edges between previously contracted parts.

Formalization scope

Twin-width is the predicate TwinWidthLE G d, never a numerical infimum, so a junk value of an empty or unbounded infimum cannot make the goal trivial. A contraction sequence must merge exactly two parts at each step and start from singletons; it cannot jump to one part. Homogeneity counts all pairs between two parts, in both of its alternatives. Boolean-width is bounded on every edge of the decomposition tree, not only at the root, and the count runs over neighbourhoods of all subsets of $A_e$ , not only of single vertices. The bound $2N-1$ depends only on $N$ , not on the graph.

Boolean-width is kept as the integer count $N=2^{\operatorname{boolw}(G)}$ ; since $\operatorname{boolw}(G)=k$ means that the least admissible count is $2^k$ , the Lean goal for this $N$ is exactly the printed theorem. Subtractions $2N-1$ are in $\mathbb N$ and exact where used. Graphs live on a Fintype vertex type with decidable equality and decidable adjacency. A graph on the empty vertex set has no decomposition tree; the goal is silent about it, and it has twin-width $0$ . No hypothesis is added to any statement relative to the page except $N\ge 1$ in milestone 2, which the page has implicitly ( $2^k\ge1$ ) and without which the conclusion is impossible.

The definitions needed are the setting module TwinWidthI.BoolWidth.Setting: merge steps, homogeneity, $d$ -partitions, twin-width, decomposition trees (DTree), the count $\nu_G$ and BoolWidthLE. Proofs of the milestones, a proof of the goal, and lemmas towards the iteration invariant are welcome.

Selected references

É. Bonnet, E. J. Kim, S. Thomassé and R. Watrigant, Twin-width I: Tractable FO Model Checking, J. ACM 69(1), Article 3, 2021. https://doi.org/10.1145/3486655
B.-M. Bui-Xuan, J. A. Telle and M. Vatshelle, Boolean-width of graphs, Theoretical Computer Science 412(39), 5187–5204, 2011. https://doi.org/10.1016/j.tcs.2011.05.022
M. Vatshelle, New Width Parameters of Graphs, PhD thesis, University of Bergen, 2012 (reference [39] of Bonnet et al.; source of the chain boolw ≤ modw ≤ cw ≤ 2^{rw+1} − 1).

6 thms3 active usersReviewed

Completed

Combinatorics·Captain: marwahaha

A proof of Seymour’s second-neighborhood conjectureOpen Problem

Motivation

An oriented graph may have very uneven outdegrees, yet the second-neighborhood conjecture asks for one vertex whose new two-step reach is at least its immediate outdegree. The source manuscript presents the surrounding research claim.

Setting

An oriented graph is a loopless asymmetric relation r on a finite nonempty vertex type. First neighbors satisfy r(v,w). Second neighbors are vertices w distinct from v, not already first neighbors, but reached by some directed path v→u→w.

Formalization target

Prove that some vertex v satisfies

|N_1^+(v)|\le|N_2^+(v)|.

Every second-neighborhood vertex is counted once, irrespective of how many two-step paths reach it.

The selected formal target is OAI.SeymourSecondNeighborhood.exists_goodVertex.

Significance and status

The statement covers all finite oriented graphs, including disconnected graphs and graphs whose underlying undirected graph is not complete. The published target is currently Open; the manuscript's argument and a checked Lean proof are separate deliverables.

Difficulty

Counting length-two walks overcounts repeated endpoints and may include first neighbors. The conclusion concerns the set of vertices at directed distance exactly two.

Formalization scope

The formal relation need not be supplied with decidability; the finite sets are formed classically. Looplessness and asymmetry are explicit hypotheses, and the vertex type is finite and nonempty. GoodVertex is exactly the finite-cardinality comparison.

Selected references

OpenAI, A proof of Seymour’s second-neighborhood conjecture, preprint, 2026. Pinned manuscript.
OpenAI, accompanying formal statements, commit adc7f1241b42. Goal source.

45 thms3 active usersReviewed

Completed

Combinatorics Probability·Captain: wurtle

A Sharp Threshold Bound for Monotone Graph PropertiesResearch Paper

Motivation: how sharp is the threshold of a graph property?

Many questions about random graphs ask when a property — connectivity, containing a triangle, having a perfect matching — appears in the Erdős–Rényi random graph $G(n,p)$ , where each of the $\binom n2$ possible edges is present independently with probability $p$ . For an increasing property the probability $\mu_p(\mathcal P)$ rises from $0$ to $1$ as $p$ grows, and the threshold width measures how quickly: the length of the interval of $p$ over which $\mu_p(\mathcal P)$ climbs from $\varepsilon$ to $1-\varepsilon$ . Friedgut and Kalai showed in 1996 that symmetry alone forces every such transition to be narrow, and conjectured the optimal universal width. This question links probabilistic combinatorics with the Fourier analysis of Boolean functions, and the influence inequalities developed for it are now standard tools in theoretical computer science and statistical physics.

Timeline

1981 — Russo's formula (the Margulis–Russo identity) expresses $\frac{d}{dp}\mu_p(\mathcal P)$ as a total influence (Russo 1981).
1988 — Kahn, Kalai and Linial prove that every balanced Boolean function has a coordinate of influence $\Omega(\log N/N)$ (KKL, FOCS 1988).
1992 — Bourgain, Kahn, Kalai, Katznelson and Linial extend the influence theorem to product measures (BKKKL, Israel J. Math. 1992).
1996 — Friedgut and Kalai prove that every monotone graph property on $n$ vertices has threshold width at most $C\log(1/(2\varepsilon))/\log n$ (Theorem 1.1) and conjecture the bound with $(\log n)^2$ in the denominator (Conjecture 1.2) (Friedgut–Kalai, Proc. AMS 1996). The property of containing a clique of order proportional to $\log n$ shows $(\log n)^{-2}$ would be optimal.
1997 — Bourgain and Kalai, using the action of the symmetry group on sets of coordinates, obtain width $C_{\eta,\varepsilon}(\log n)^{-2+\eta}$ for every $\eta>0$ (Bourgain–Kalai, GAFA 1997).
2020 — Kelman, Kindler, Lifshitz, Minzer and Safra prove, at $p=1/2$ , the graph-symmetric influence bound $I_{1/2}(f)\ge c\,(\log n)^2(\log\log n)^{-2}\operatorname{Var}_{1/2}(f)$ (KKLMS, GAFA 2020).
2022 — Friedgut surveys the influence method (ICM 2022).
2026 — An OpenAI preprint, A Sharp Threshold Bound for Monotone Graph Properties (OpenAI Math Release, September 25, 2026), claims the conjectured bound with explicit constant $2^{19}$ . The preprint has not been peer reviewed and its theorem is not formally verified.

Setting

Fix an integer $n\ge2$ and let $E_n=\binom{[n]}{2}$ be the set of unordered pairs of vertices. A graph configuration is a map $x:E_n\to\{0,1\}$ (in Lean GraphConfig n := GraphEdge n → Bool, where GraphEdge n is the type of 2-element subsets of Fin n). A Boolean function $f$ on configurations is

vertex invariant if $f(\pi\cdot x)=f(x)$ for every permutation $\pi$ of the vertices, where $\pi$ acts on edges by relabelling endpoints;
increasing if $x\le y$ edgewise and $f(x)=1$ imply $f(y)=1$ ;
nontrivial if it takes both values.

For $p\in\mathbb R$ the graph mean is $\mu_p(f)=\sum_x \prod_{e} p^{x_e}(1-p)^{1-x_e}\, f(x)$ , the probability that $G(n,p)$ has the property when $p\in[0,1]$ . For $0<a<1$ the quantile is

p_a(f)=\inf\{p\in[0,1]:\ \mu_p(f)\ge a\}.

Formalization targets

Goal: the Friedgut–Kalai sharp-threshold conjecture (Theorem 1.1)

For every $n\ge2$ , every vertex-invariant, increasing, nontrivial $f$ , and every $0<\varepsilon<1/2$ ,

p_{1-\varepsilon}(f)-p_\varepsilon(f)\ \le\ \frac{2^{19}}{(\log n)^2}\,\log\frac{1}{2\varepsilon}.

The constant $2^{19}$ is the source's explicit choice and is not claimed to be sharp; the content is the order $(\log n)^{-2}$ with linear dependence on $\log(1/(2\varepsilon))$ . The goal statement is published on the platform with status Open: no machine-checked proof exists yet.

Significance

The result itself. The bound is uniform over all monotone graph properties and is of optimal order in $n$ for fixed $\varepsilon$ , as the clique example of Friedgut and Kalai shows. It settles the exponent question left open between the $(\log n)^{-1}$ bound of 1996 and the $(\log n)^{-2+\eta}$ bound of 1997. The driving estimate in the source, Theorem 1.2 (variance is at most $2^{17}(\log n)^{-2}$ times total influence, for every $0<p<1$ and without monotonicity), is a graph-symmetric influence inequality of independent interest; it removes the $(\log\log n)^2$ loss of the 2020 bound and holds at every bias.

Formalizing it. A formal proof would certify a universal statement over all graph properties with an explicit constant. The supporting library — Fourier–Walsh analysis on biased product spaces, pivotal influences, the Margulis–Russo derivative formula, and random restrictions — is reusable for other threshold and influence results, none of which are currently formalized in Mathlib in this form.

Difficulty

The classical route bounds the derivative $\frac{d}{dp}\mu_p$ from below through the largest influence, using only that the symmetry group acts transitively on edges; transitivity alone cannot give better than $(\log n)^{-1}$ , because there are transitive families (on non-graph coordinate sets) whose thresholds are that wide. Reaching $(\log n)^{-2}$ requires using the vertex structure of the symmetry group, and the bound must hold uniformly for every bias $p\in(0,1)$ , including very small $p$ where hypercontractive estimates degrade. Influence estimates at $p=1/2$ alone do not suffice, since a width bound requires control throughout the transition interval.

Formalization scope

Configurations are GraphEdge n → Bool; the measure is the explicit finite sum graphMean p f with product weights $p$ or $1-p$ ; logarithms are natural (Real.log).
graphQuantile a f is sInf of $\{p\in[0,1]:\mu_p(f)\ge a\}$ . For a nontrivial increasing $f$ , $\mu_1(f)=1$ , so this set is nonempty and the infimum is not a junk value; the hypotheses NontrivialGraphProperty and $0<\varepsilon<1/2$ exclude the degenerate cases.
The theorem quantifies over all $n\ge 2$ , all such $f$ , and all real $\varepsilon\in(0,1/2)$ ; no asymptotic or "sufficiently large $n$ " assumption is used.
Needed infrastructure: biased Fourier expansion on $\{0,1\}^{E_n}$ , influences and the Russo derivative formula, the action of $S_n$ on edges, and integration of a differential inequality for the quantile. Contributions formalizing Theorem 1.2 (variance–influence) or Russo's formula separately are welcome as stepping stones.

Selected references

E. Friedgut and G. Kalai, Every monotone graph property has a sharp threshold, Proc. Amer. Math. Soc. 124 (1996), 2993–3002. https://doi.org/10.1090/S0002-9939-96-03732-X
J. Bourgain and G. Kalai, Influences of variables and threshold intervals under group symmetries, Geom. Funct. Anal. 7 (1997), 438–461. https://doi.org/10.1007/s000390050015
J. Kahn, G. Kalai and N. Linial, The influence of variables on Boolean functions, FOCS 1988, 68–80. https://doi.org/10.1109/SFCS.1988.21923
J. Bourgain, J. Kahn, G. Kalai, Y. Katznelson and N. Linial, The influence of variables in product spaces, Israel J. Math. 77 (1992), 55–64. https://doi.org/10.1007/BF02808010
L. Russo, On the critical percolation probabilities, Z. Wahrsch. Verw. Gebiete 56 (1981), 229–237. https://doi.org/10.1007/BF00535742
E. Kelman, G. Kindler, N. Lifshitz, D. Minzer and M. Safra, Towards a proof of the Fourier–entropy conjecture?, Geom. Funct. Anal. 30 (2020), 1097–1138. https://doi.org/10.1007/s00039-020-00544-2
E. Friedgut, KKL's influence on me, Proc. ICM 2022, Vol. 6, 4568–4581. https://doi.org/10.4171/ICM2022/78
OpenAI, A Sharp Threshold Bound for Monotone Graph Properties, OpenAI Math Release preprint, September 25, 2026 (source of the goal; Theorem 1.1, p. 1). https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/A-Sharp-Threshold-Bound-for-Monotone-Graph-Properties-September-25-2026/paper.pdf

37 thms3 active usersReviewed

Completed

Markov Chain Probability·Captain: mikedeng1

Geometric Bounds for Eigenvalues of Markov Chains 2: Odd Closed Paths Bound the Smallest Eigenvalue, β_min ≥ −1 + 2/ιResearch Paper

Motivation

The speed at which a finite reversible Markov chain approaches its stationary distribution is controlled by its eigenvalues. For a chain with eigenvalues $1=\beta_0>\beta_1\ge\dots\ge\beta_{m-1}\ge-1$ , the distance to stationarity after $n$ steps is governed by $\beta_*^{\,n}$ , where $\beta_*=\max(\beta_1,|\beta_{m-1}|)$ (Diaconis and Stroock 1991, Proposition 3). Upper bounds on the second eigenvalue $\beta_1$ are the familiar half of this picture, and they are what Cheeger-type and Poincaré inequalities provide. The other half is the smallest eigenvalue $\beta_{\min}=\beta_{m-1}$ : a chain whose smallest eigenvalue is close to $-1$ oscillates almost periodically and mixes slowly whatever $\beta_1$ is. A chain is aperiodic exactly when $\beta_{\min}>-1$ , but that qualitative fact gives no rate.

Diaconis and Stroock's paper gives geometric bounds for both ends of the spectrum, expressed through systems of paths in the graph of the chain. Their bound on $\beta_{\min}$ uses closed paths with an odd number of edges, the combinatorial witnesses of aperiodicity. The paper has been a standard reference for path (canonical-path, multicommodity-flow) methods in the analysis of Markov chain Monte Carlo since its publication.

Timeline:

1988–1989, Jerrum and Sinclair: conductance (Cheeger-type) bounds on $\beta_1$ for chains on combinatorial structures.
1991, Diaconis and Stroock: path bounds for $\beta_1$ (Proposition 1, the Poincaré inequality $\beta_1\le1-1/\kappa$ ) and for $\beta_{\min}$ (Proposition 2, this mission), with the specializations to random walks on graphs (Corollaries 1 and 2).

Setting

Let $X$ be a finite set and $P(x,y)$ the transition matrix of an irreducible Markov chain on $X$ , reversible with respect to a probability distribution $\pi$ :

Q(x,y)=\pi(x)P(x,y)=\pi(y)P(y,x)\qquad(x,y\in X).

The operator $(P\varphi)(x)=\sum_yP(x,y)\varphi(y)$ is self-adjoint on $L^2(\pi)$ , with inner product $\langle\varphi,\psi\rangle_{L^2(\pi)}=\sum_x\varphi(x)\psi(x)\pi(x)$ , so its eigenvalues are real. Write $E(\varphi^2)=\sum_x\varphi(x)^2\pi(x)$ and let $\beta_{\min}$ be the smallest eigenvalue of $P$ .

The graph of the chain has vertex set $X$ , an edge from $x$ to $y$ when $Q(x,y)>0$ , and a self-loop at $x$ when $Q(x,x)>0$ . An odd closed path $\sigma_x$ at $x$ is a sequence of edges from $x$ back to $x$ , with an odd number of edges, in which no directed edge is traversed twice. Its length is

|\sigma_x|_Q=\sum_{e\in\sigma_x}Q(e)^{-1}.

A system of odd paths $\Sigma=(\sigma_x)_{x\in X}$ chooses one such path for every point, and its load is

\iota=\iota(\Sigma)=\max_e\sum_{\sigma_x\ni e}|\sigma_x|_Q\,\pi(x),

the maximum over directed edges $e$ of the weighted length of the paths through $e$ (display (1.7) of the paper).

For the random walk on a graph $G=(X,E)$ , $P(x,y)=1/d(x)$ when $\{x,y\}\in E$ , with $d(x)$ the degree, and $\pi(x)=d(x)/2|E|$ . There $d_*$ is the maximum degree, $\sigma_*$ the largest number of edges of a path in $\Sigma$ , and $b_*=\max_e\sharp\{\sigma\in\Sigma:e\in\sigma\}$ .

Formalization targets

Goal: Proposition 2

For an irreducible, aperiodic, reversible chain and every system $\Sigma$ of odd closed paths,

\beta_{\min}\ge-1+\frac{2}{\iota(\Sigma)}.

Milestones (the steps of the paper's proof)

The identity (1.8): $\tfrac12\sum_{x,y}(\varphi(x)+\varphi(y))^2Q(x,y)=E(\varphi^2)+\langle\varphi,P\varphi\rangle_{L^2(\pi)}$ .
Along an odd closed path $x,y,w,\dots,z,x$ : $\varphi(x)=\tfrac12\{(\varphi(x)+\varphi(y))-(\varphi(y)+\varphi(w))+\dots+(\varphi(z)+\varphi(x))\}$ .
For every $\varphi$ : $E(\varphi^2)\le\frac{\iota}{2}\big(E(\varphi^2)+\langle\varphi,P\varphi\rangle_{L^2(\pi)}\big)$ .
Every eigenvalue $\beta$ of $P$ satisfies $\beta\ge-1+2/\iota$ .

Companions

Corollary 2. For the random walk on a connected, non-bipartite graph and any system $\Sigma$ of odd paths, $\beta_{\min}\ge-1+\dfrac{2}{d_*\sigma_*b_*}$ .
Remark 1.3. With odd paths $\sigma_{xy}$ for every ordered pair and $\tilde\iota=\max_e\sum_{\sigma_{xy}\ni e}|\sigma_{xy}|_Q\pi(x)\pi(y)$ : $\beta_{\min}\ge-1+1/\tilde\iota$ .

Significance

Proposition 2 turns aperiodicity into a number. With Proposition 1, which bounds $\beta_1\le1-1/\kappa$ through paths between pairs of points, it bounds the absolute spectral gap $1-\beta_*$ entirely in terms of path geometry, and so bounds the variation distance to stationarity through Proposition 3. Corollary 2 is the form most often applied: for a random walk on a non-bipartite graph, a choice of short odd cycles that do not crowd any single edge certifies that the walk does not oscillate.

Proposition 2 and its corollary are proved in the paper. As far as a search of the platform shows, no machine-checked proof exists. The platform already has the vocabulary (stochastic matrices, stationarity, reversibility, eigenvalues and the $L^2(\pi)$ inner product, from the published Levin–Peres–Wilmer layer) and the qualitative fact that $-1$ is not an eigenvalue of an irreducible aperiodic chain. This mission adds the quantitative bound, the identity (1.8), and the path inequality, all reusable for other path-based eigenvalue estimates.

Difficulty

Each step is elementary, but the bookkeeping is where a proof can go wrong. The Cauchy–Schwarz step is applied along each path separately, and the resulting double sum over points and over the edges of their paths must be exchanged into a sum over edges. That exchange is exact only if each path traverses each directed edge at most once. A path that crosses an edge twice contributes twice, while $\iota$ counts it once. Self-loops are edges here, and the sum over directed edges in the last step must match the sum over ordered pairs $(x,y)$ , including $x=y$ , in the identity (1.8). The alternating signs work only because the number of edges is odd; an even closed path cancels $\varphi(x)$ instead of doubling it.

The bound is also only as good as the chosen paths: short odd cycles that spread their load over many edges give a small $\iota$ , and the choice of $\Sigma$ is part of every application.

Formalization scope

The chain is a real matrix P : Matrix V V ℝ on a Fintype V, with the published predicates IsStochastic, Irreducible, Aperiodic, IsStationary (which includes that $\pi$ is a probability vector) and DetailedBalance. $Q$ is edgeMeasure, the inner product innerPi, eigenvalues IsEigenvalue (a real eigenvalue with a nonzero real eigenfunction). $\beta_{\min}$ is the infimum of the real eigenvalues of $P$ , a minimum for a stochastic matrix on a nonempty set.

Paths are vertex lists. A path traverses the directed edges between consecutive vertices, each with $Q>0$ . The paper defines $|\sigma_x|_Q$ "by analogy with (1.4)", whose paths may not repeat an edge. For the directed edges of §1C this rule is read as "no directed edge twice". Under the unordered reading a vertex of degree one would have no odd closed path, contradicting the page's remark that such paths always exist for irreducible aperiodic chains. $\iota$ is a real supremum over the finite set of directed edges with $Q>0$ , and it is $0$ only when there is no edge. A system of odd paths on a nonempty set excludes that case, so the bound is never reduced to $\beta_{\min}\ge-1$ by $2/0=0$ . The system $\Sigma$ is a universally quantified hypothesis of every statement, never an existential one. No milestone assumes the inequality of milestone 3 or the identity (1.8) as a hypothesis. No assumption $|X|\ge2$ is made.

Milestones 3 and 4 do not assume aperiodicity: the existence of an odd path system implies it. The identity (1.8) assumes only stochasticity and stationarity. Corollary 2 assumes only that the graph is connected and not 2-colorable; the chain properties follow from these. In Corollary 2, $b_*$ counts paths through a directed edge, which is at most the count through the unordered edge, so the stated bound implies the one with the unordered count. Only the first half of Remark 1.3 is stated; its second half needs Proposition 1's quantity, which belongs to another mission of the series.

Contributions welcome: proofs of the milestones in order, a general Cauchy–Schwarz-along-paths lemma shared with the Poincaré inequality, and the existence of odd path systems for irreducible aperiodic chains.

Selected references

P. Diaconis and D. Stroock, Geometric bounds for eigenvalues of Markov chains, Ann. Appl. Probab. 1(1):36–61, 1991. https://doi.org/10.1214/aoap/1177005980
A. Sinclair and M. Jerrum, Approximate counting, uniform generation and rapidly mixing Markov chains, Inform. and Comput. 82(1):93–133, 1989. https://doi.org/10.1016/0890-5401(89)90067-9
D. A. Levin, Y. Peres and E. L. Wilmer, Markov Chains and Mixing Times, American Mathematical Society, 2009 (2nd ed. 2017). https://doi.org/10.1090/mbk/107

12 thms3 active usersReviewed

Completed

Combinatorics·Captain: mikedeng1

The Four-Colour Theorem: Birkhoff's Lemma (6.4) — Every Non-Empty Consistent Set of Edge-Colourings of a Ring of Length 5 Meeting ℰ Includes One of 𝒞ᵢ, 𝒟ᵢ, ℰResearch Paper

Motivation

The Four-Colour Theorem was proved by Appel and Haken (1976–77) and re-proved by Robertson, Sanders, Seymour and Thomas (RSST, 1997) with a simpler, fully computer-checkable argument. Both proofs rest on reducibility: a configuration is reducible when every 4-colouring of the ring around it can be modified, by Kempe-chain recolouring, into one that extends inside. RSST make this precise with a purely combinatorial notion, the consistent set of edge-colourings of a circuit (§3 of their paper), which captures exactly which boundary colourings Kempe interchanges can reach from one another.

The oldest results about consistent sets predate the computer proofs. G. D. Birkhoff (1913) analysed rings of length 4 and 5 and showed that the possible "Kempe-closed" sets of boundary colourings on such short rings are very restricted. RSST restate Birkhoff's analysis in their language as (6.3) (rings of length 4) and (6.4) (rings of length 5). These two lemmas power the short-circuit subroutine of their quadratic 4-colouring algorithm (6.5), which colours a triangulation across a separating circuit of length 4 or 5.

Timeline:

1879–1890. Kempe introduces chain interchanges; Heawood finds the gap in Kempe's argument.
1913. Birkhoff, The reducibility of maps, studies rings of small size and introduces reducibility.
1976–77. Appel and Haken prove the Four-Colour Theorem.
1997. Robertson, Sanders, Seymour and Thomas give a new proof and an $O(n^2)$ colouring algorithm; consistent sets and lemmas (6.3), (6.4) appear in §§3 and 6.
2005–08. Gonthier formalizes the Four-Colour Theorem in Coq, with a different encoding of Kempe closure (chromograms on hypermaps).

Setting

Let $R$ be a circuit of length $k$ : a cycle with edges $e_1, \dots, e_k$ in order, with no repeated vertices or edges. An edge-colouring of $R$ is a map $\kappa : E(R) \to \{-1, 0, 1\}$ .

A match is an unordered pair $\{e, f\}$ of distinct edges, and a signed match is a pair $(\{e,f\}, \mu)$ with $\mu = \pm 1$ . A signed matching is a set $M$ of signed matches such that for any two distinct members $(\{e,f\},\mu)$ , $(\{e',f'\},\mu')$ : the pairs $\{e,f\}$ and $\{e',f'\}$ are disjoint, and $e, f$ lie in the same component of $R$ with $e'$ and $f'$ deleted. Write $E(M)$ for the edges covered by $M$ .

For $\theta \in \{-1,0,1\}$ , the colouring $\kappa$ $\theta$ -fits $M$ when $E(M)$ is exactly the set of edges with $\kappa(e) \neq \theta$ , and for each $(\{e,f\},\mu) \in M$ , $\kappa(e) = \kappa(f)$ holds if and only if $\mu = 1$ . A set $\mathcal C$ of edge-colourings is consistent if for every $\kappa \in \mathcal C$ and every $\theta$ there is a signed matching $M$ that $\kappa$ $\theta$ -fits such that $\mathcal C$ contains every edge-colouring that $\theta$ -fits $M$ .

Two edge-colourings are equivalent if one is obtained from the other by a permutation $\lambda$ of $\{-1,0,1\}$ . On the circuit of length 5, $\mathcal A_{ij}$ ( $i \neq j$ ) is the equivalence class of the colouring that is $1$ on $e_i$ , $-1$ on $e_j$ and $0$ elsewhere. Then $\mathcal C_i = \mathcal A_{ij} \cup \mathcal A_{ik} \cup \mathcal A_{jk}$ , where $e_j, e_k$ are the two edges sharing an end with $e_i$ ; $\mathcal D_i = \mathcal A_{ac} \cup \mathcal A_{ad} \cup \mathcal A_{bc} \cup \mathcal A_{bd}$ , where $e_a, e_b, e_c, e_d$ are the other edges in order; and $\mathcal E = \mathcal A_{12} \cup \mathcal A_{23} \cup \mathcal A_{34} \cup \mathcal A_{45} \cup \mathcal A_{15}$ . In Lean these are A, C5, D5, E5, and Consistent.

Formalization targets

Goal: Birkhoff's lemma for rings of length 5, (6.4)

\mathcal C \text{ consistent},\ \mathcal C \neq \emptyset,\ \mathcal C \cap \mathcal E \neq \emptyset \;\Longrightarrow\; \exists i,\ \mathcal C_i \subseteq \mathcal C \ \ \text{or}\ \ \exists i,\ \mathcal D_i \subseteq \mathcal C \ \ \text{or}\ \ \mathcal E \subseteq \mathcal C.

Milestones

Every consistent set is a union of equivalence classes (§6, p. 25): $\kappa \in \mathcal C \Rightarrow [\kappa] \subseteq \mathcal C$ .
Claim (1) of the proof of (6.4): if $\mathcal A_{12} \subseteq \mathcal C$ then $\mathcal C$ includes one of $\mathcal A_{13}, \mathcal A_{15}$ and one of $\mathcal A_{23}, \mathcal A_{25}$ .
Claim (2): if $\mathcal A_{13} \subseteq \mathcal C$ then $\mathcal C$ includes one of $\mathcal A_{23}, \mathcal A_{35}$ .
The closure facts of §3, p. 8: $\emptyset$ is consistent, unions of two consistent sets are consistent, and every set $\mathcal S$ has a unique maximal consistent subset $\mathcal S'$ .

Companion: Birkhoff's lemma for rings of length 4, (6.3)

With $\mathcal C_0, \dots, \mathcal C_3$ the classes of $(0,0,0,0)$ , $(0,1,1,0)$ , $(0,1,0,1)$ , $(0,0,1,1)$ , every non-empty consistent set includes one of $\mathcal C_0 \cup \mathcal C_1$ , $\mathcal C_1 \cup \mathcal C_2$ , $\mathcal C_2 \cup \mathcal C_3$ , $\mathcal C_3 \cup \mathcal C_0$ .

Significance

The result. (6.3) and (6.4) say that on rings of length at most 5 the Kempe-closed families of boundary colourings are rigid: a non-empty consistent family always contains one of a short explicit list of families. This is what makes separating circuits of length 4 and 5 harmless in a minimal counterexample and in the RSST colouring algorithm: whatever colourings one side of the circuit admits, the other side can be made to agree after Kempe changes.

Formalizing it. The Four-Colour Theorem itself is machine-checked (Gonthier, Coq), but that proof uses a different combinatorial encoding; RSST's notion of a consistent set, their signed matchings, and Birkhoff's ring lemmas in their formulation have no machine-checked version. The Four-Colour Theorem as such is not part of this mission; it is posed separately on the platform as the open goal FourColor.four_color. This mission builds the self-contained §3 layer (consistency) that RSST's reducibility computations rest on, proves two of its basic structural facts, and proves the two Birkhoff lemmas the paper uses. The definitions are reusable for a later formalization of (3.1) (lifts of tri-colourings form a consistent set) and of D-reducibility.

Difficulty

The statements are about finite objects: on a 5-ring there are $3^5 = 243$ edge-colourings, and the signed matchings have at most two matches. The difficulty lies elsewhere. Consistency quantifies over every member of $\mathcal C$ , every $\theta$ and the existence of a signed matching together with a closure property, so a consistent set cannot be checked locally. The component condition on signed matchings is a statement about connectivity in a graph with two edges deleted, which must be connected to elementary arithmetic on the cycle before anything can be computed. An argument by brute force over all $2^{243}$ subsets is infeasible, so a proof has to pass through the structure of the classes $\mathcal A_{ij}$ . The paper's own proof also uses the dihedral symmetry of the 5-ring without stating it as a lemma; it is not a milestone.

Formalization scope

The circuit of length $k$ is SimpleGraph.cycleGraph k on Fin k; its edges are indexed by Fin k, edge $i$ being $\{i, i+1\}$ (mod $k$ ). The paper's $e_i$ is edge $i-1$ : $\mathcal A_{12}$ is A 0 1, $\mathcal A_{15}$ is A 0 4, $\mathcal A_{25}$ is A 1 4, $\mathcal A_{35}$ is A 2 4.
Colours are Mathlib's SignType; an edge-colouring is Fin k → SignType; $\mu \in$ ℤˣ; a match is a non-diagonal Sym2 (Fin k) of edge indices; a signed matching is a Set.
The component condition is encoded literally with deleteEdges and Reachable, for both orders of every distinct pair; both halves of "consistent" are kept; equivalence uses Equiv.Perm SignType.
C5 i uses edges $i \pm 1$ ; D5 i uses $(a,b,c,d) = (i+1, i+2, i+3, i+4)$ mod 5, the order along the path $R - e_i$ , which is the reading the paper's proof requires ( $\mathcal D_4 \supseteq \mathcal A_{25}, \mathcal A_{12}, \mathcal A_{13}, \mathcal A_{35}$ ).
General- $k$ statements assume $k \ge 3$ : circuits of length at most 2 have parallel edges and are not cycle graphs.
Ruled out: dropping the component condition (crossing pairs would become signed matchings), a one-sided "consistent" (every set would be consistent and (6.4) false), any use of the junk class A i i, and degenerate circuits.

All definitions are in one file, FourColourRSST.Ring.Setting. Proofs of any item are welcome, as are lemmas making consistency decidable on small rings and the symmetry of the 5-ring under rotations and reflections.

Selected references

N. Robertson, D. P. Sanders, P. Seymour, R. Thomas, The Four-Colour Theorem, J. Combin. Theory Ser. B 70 (1997), 2–44. https://doi.org/10.1006/jctb.1997.1750
G. D. Birkhoff, The reducibility of maps, Amer. J. Math. 35 (1913), 115–128. https://doi.org/10.2307/2370276
K. Appel, W. Haken, Every planar map is four colorable. Part I: Discharging, Illinois J. Math. 21 (1977), 429–490. https://doi.org/10.1215/ijm/1256049011
G. Gonthier, Formal proof — the Four-Color Theorem, Notices Amer. Math. Soc. 55 (2008), 1382–1393. https://www.ams.org/notices/200811/tx081101382p.pdf

6 thms3 active usersReviewed

Completed

Linear Optimization Theoretical Computer Science·Captain: mikedeng1

Multicommodity Max-Flow Min-Cut Theorems and Their Use in Designing Approximation Algorithms I: Every Uniform Multicommodity Flow Problem Has Ω(𝒮/log n) ≤ f ≤ 𝒮Research Paper

Motivation

A multicommodity flow problem asks to route several commodities simultaneously through a capacitated network, each from its own source to its own sink. For a single commodity, the max-flow min-cut theorem of Ford and Fulkerson says that the largest routable flow equals the capacity of the smallest separating cut. For many commodities the natural analogue fails: the max-flow can be strictly smaller than the min-cut, already for four commodities (Okamura and Seymour, 1981). Leighton and Rao asked how large the gap can be, and showed that for uniform demands it is at most logarithmic in the number of nodes. The result turned the min-cut, an NP-hard quantity, into something approximable by a linear program, and became the basis of the first polylogarithmic approximation algorithms for sparsest cut, balanced cut, minimum feedback arc set, crossing number and VLSI layout (Leighton–Rao, J. ACM 1999).

Timeline:

1956–1963. Ford and Fulkerson prove max-flow = min-cut for one commodity; Hu (1963) proves equality for two commodities.
1981–1990. Okamura and Seymour give a 4-commodity example with max-flow 3/4 and min-cut 1. Schrijver (1990), combining Lomonosov and Papernov, characterizes demand graphs for which equality always holds. Shahrokhi and Matula (1990) prove equality for uniform demands under a condition on the dual.
1988. Leighton and Rao (FOCS 1988) prove the $\Theta(\log n)$ gap for uniform demands; the journal version (1999) is the source of this mission.
1995. Linial, London and Rabinovich, and independently Aumann and Rabani, extend the bound to arbitrary demands with $O(\log k)$ for $k$ commodities, via metric embeddings (Combinatorica 1995).

Setting

A network is a finite set $V$ of $n$ nodes with a capacity $C(u,v)=C(v,u)\ge0$ for every pair; the pair is an edge when $C(u,v)>0$ . For $U\subseteq V$ with complement $\bar U$ , the cut capacity $C(U,\bar U)$ is the total capacity of the edges joining $U$ to $\bar U$ . As in the paper, the network is assumed connected: $C(U,\bar U)>0$ for every nonempty proper $U$ .

In the uniform multicommodity flow problem (UMFP) every unordered pair of nodes is a commodity with demand one. A routing of value $\lambda$ sends $\lambda$ units between every pair simultaneously, so that the total flow of all commodities over each edge, in both directions together, is at most its capacity. The max-flow $f$ is the largest such $\lambda$ (the concurrent max-flow).

The min-cut (sparsest cut) of the UMFP is

\mathcal S=\min_{\emptyset\ne U\subsetneq V}\frac{C(U,\bar U)}{|U|\,|\bar U|},

the minimum over cuts of the cut capacity divided by the demand separated by the cut. The quantity $C(U,\bar U)/(|U||\bar U|)$ is the ratio cost of the cut.

The milestones use the dual objects. A distance function $d$ assigns a nonnegative length to each edge; $d(u,v)$ is then the shortest-path distance, $d(T,u)=\min_{t\in T}d(t,u)$ , and the total weight is $W=\sum_{e}C(e)d(e)$ . The distance constraint (5) is $\sum_{\{u,v\}}d(u,v)\ge1$ , summed over unordered pairs. A set of nodes has radius at most $\Delta$ if some centre reaches all its nodes by walks inside the set of length at most $\Delta$ . Throughout, $\log n=\log_2 n$ .

Formalization targets

Goal: Theorem 2 (p. 795)

\Omega\!\left(\frac{\mathcal S}{\log n}\right)\le f\le\mathcal S

for every uniform multicommodity flow problem: there is one absolute constant $c>0$ such that $c\,\mathcal S/\log n\le f\le\mathcal S$ for every connected network with $n\ge2$ nodes. The goal fixes no constant, so it is the form any improved argument would still prove.

Milestones, in the order the argument uses them

Weak duality (§1.2, pp. 789–790): every concurrent flow of value $\lambda$ satisfies $\lambda\,|U||\bar U|\le C(U,\bar U)$ for every cut.
LP duality (§2.2, p. 796): every distance function satisfying (5) has $W\ge f$ , and some such function has $W=f$ .
Lemma 3 (p. 797): for every $\Delta>0$ , $V$ splits into components of radius at most $\Delta$ with at most $4W\log n/\Delta$ capacity between components.
Corollary 4 (pp. 798–799): either a set of at least $2n/3$ nodes has radius at most $1/(2n^2)$ , or some cut has ratio cost at most $36W\log n$ .
Lemma 5 (p. 799): if $|T|\ge 2n/3$ and $\sum_{u\notin T}d(T,u)\ge 1/(2n)$ , some cut has ratio cost at most $6W$ .
Lemma 6 (p. 800): a distance function satisfying (5) yields a cut of ratio cost at most $36W\log n$ .

Companion

$\mathcal S\le 36\,f\log n$ and $f\le\mathcal S$ : Theorem 2 with the constant its proof produces.

Significance

The theorem says that the LP relaxation of uniform sparsest cut has integrality gap $O(\log n)$ , and the expander example of §2.1 (Theorem 1) shows this is tight. Combined with the cut-finding argument, it gives an $O(\log n)$ -approximation for sparsest cut and, through the paper's Section 3, approximation algorithms for balanced separators, minimum cut linear arrangement, crossing number, VLSI layout area, feedback arc set and the emulation of networks. Region-growing decompositions of the kind in Lemma 3 reappear in low-diameter decompositions, multicut (Garg–Vazirani–Yannakakis), and metric embedding.

The result is proved; no machine-checked proof of it is known. A formalization would provide: concurrent multicommodity flow and its LP dual on finite graphs, the uniform sparsest cut, a verified region-growing decomposition, and the max-flow min-cut gap theorem itself. The LP-duality milestone, which the paper cites rather than proves, is a reusable piece of flow theory in its own right.

Difficulty

The upper bound $f\le\mathcal S$ is a counting argument. The lower bound is the content. The natural idea, rounding an optimal dual distance function by a threshold and cutting the long edges, does not work: the paper notes (p. 797) that no thresholding rule is known that always yields a good cut, because edges with large distance need not form a sparse cut. Any argument must convert the fractional dual into a single cut while losing only a $\log n$ factor against the total weight $W$ , which requires a global property of the distance function rather than the lengths of individual edges. The LP-duality step needs a correct dual for the concurrent flow problem with shortest-path distances, which Mathlib does not provide off the shelf.

Formalization scope

Nodes and capacities. V is a Fintype with decidable equality; capacities are a symmetric nonnegative real function vanishing on the diagonal, and the graph is the simple graph of pairs with positive capacity. Goal-level statements assume 2 ≤ Fintype.card V and connectivity in the form $C(U,\bar U)>0$ for every nonempty proper $U$ (the paper's standing assumption, p. 789).
Demands and flows. Each unordered pair is encoded as two ordered commodities with demand $\tfrac12$ (the paper's footnote 2). Flows are arc flows with conservation per commodity, and both directions of an edge share its capacity. The max-flow is the real supremum of feasible values; with $n\ge2$ that set is nonempty and bounded.
Cuts. The min-cut ranges over nonempty proper subsets only. Including $U=\emptyset$ or $U=V$ would give $0/0$ , which Lean evaluates to $0$ and which would make the goal trivially true; this formalization excludes it.
Distances. $d(u,v)$ is an infimum over walks in the graph, meaningful under connectivity; the radius of a component is measured by walks inside it.
Constants. The goal keeps the page's $\Omega$ with a single universal constant chosen before the network. The milestones carry the constants computed in the paper's proofs ( $36$ in Corollary 4 and Lemma 6, $6$ in Lemma 5), and each statement says so.
Algorithms. "We can find" is formalized as existence. Running times and the remark that the proofs yield polynomial-time algorithms (p. 801) are out of scope.

Contributions welcome: proofs of any milestone; a general LP-duality theorem for concurrent multicommodity flow, reusable for the product and directed variants; and a general region-growing lemma.

Selected references

T. Leighton and S. Rao, Multicommodity max-flow min-cut theorems and their use in designing approximation algorithms, J. ACM 46(6):787–832, 1999. https://doi.org/10.1145/331524.331526
F. Shahrokhi and D. W. Matula, The maximum concurrent flow problem, J. ACM 37(2):318–334, 1990. https://doi.org/10.1145/77600.77620
H. Okamura and P. D. Seymour, Multicommodity flows in planar graphs, J. Combin. Theory Ser. B 31:75–81, 1981. https://doi.org/10.1016/S0095-8956(81)80012-3
N. Linial, E. London and Y. Rabinovich, The geometry of graphs and some of its algorithmic applications, Combinatorica 15(2):215–245, 1995. https://doi.org/10.1007/BF01200757
V. Chvátal, Linear Programming, W. H. Freeman, 1983.

10 thms3 active usersReviewed

Completed

Combinatorics Operations Research Optimization·Captain: mikedeng1

Sequencing a One State-Variable Machine: A Solvable Case of the Traveling Salesman Problem 2: For g = 0 ≤ f, the Tour ψ′ Minimizes the Largest Changeover CostResearch Paper

Motivation

A machine whose condition is described by one real number — the temperature of a furnace, the setting of a cutting knife — must process $N$ jobs in some order. Job $i$ must be started in state $A_i$ and leaves the machine in state $B_i$ ; moving the state between jobs costs money. Ordering the jobs so that the machine returns to its starting job after the last one is a traveling salesman problem whose distance matrix has a special structure. P. C. Gilmore and R. E. Gomory showed in 1964 (Oper. Res. 12(5), 655–679) that this special traveling salesman problem can be solved exactly with $O(N^2)$ operations, one of the first nontrivial polynomially solvable cases of the problem.

The same paper also treats a second objective: instead of the total changeover cost, minimize the largest single changeover cost of the cycle. This is the bottleneck traveling salesman problem, relevant whenever the binding constraint is the worst transition (a maximal temperature swing, a longest retooling) rather than the total. Without the tour constraint it is the bottleneck assignment problem solved by O. Gross (RAND, 1959). Gilmore and Gomory solve the bottleneck tour problem for the cost matrix of their model when only increases of the state cost anything. This mission formalizes that solution.

Timeline: Gross (1959) solves the bottleneck assignment problem; Gilmore and Gomory (1964) solve the sum and bottleneck traveling salesman problems for one state-variable costs; Gilmore, Lawler and Shmoys survey the well-solved special cases of the traveling salesman problem in The Traveling Salesman Problem (Wiley, 1985), where this case is a standard entry.

Setting

There are $N = n+1$ jobs. Job $i$ has a starting state $A_i\in\mathbb R$ and a final state $B_i\in\mathbb R$ , and the jobs are numbered so that $B_1\le B_2\le\dots\le B_N$ . Given two cost densities $f, g:\mathbb R\to\mathbb R$ , the cost of having job $j$ follow job $i$ is

c_{ij} = \int_{B_i}^{A_j} f(x)\,dx \ \text{ if } A_j\ge B_i,\qquad c_{ij} = \int_{A_j}^{B_i} g(x)\,dx \ \text{ if } B_i > A_j .

A permutation $\psi$ of the jobs means "job $\psi(i)$ follows job $i$ ". It is a tour if $\psi(s)\ne s$ for every nonempty proper subset $s$ of the jobs, i.e. if $\psi$ is a single cycle. The bottleneck cost of $\psi$ is

m(\psi) = \max_{1\le i\le N} c_{i\psi(i)} .

The bottleneck case of the paper is $g = 0$ and $f\ge 0$ : lowering the state is free, raising it costs $\int f$ .

A permutation $\varphi$ ranks the $A$ 's if $j>i$ implies $A_{\varphi(j)}\ge A_{\varphi(i)}$ . An interchange $\alpha_{ij}$ is the transposition of $i$ and $j$ ; $\psi\alpha_{ij}$ means "first apply $\alpha_{ij}$ , then $\psi$ ". The graph $G_\varphi$ has the jobs as nodes and an undirected arc $R_{i\varphi(i)}$ for each $i$ ; $R_{q,q+1}$ is the arc joining consecutive nodes $q$ and $q+1$ . A spanning tree of $G_\varphi$ is a set $T$ of arcs $R_{q,q+1}$ such that $G_\varphi\cup T$ is connected and no proper subset of $T$ connects $G_\varphi$ . In the bottleneck case the arc $R_{q,q+1}$ is given the cost $c_{q\varphi(q+1)}$ , and a minimum spanning tree minimizes the sum of these costs. If its arcs are $R_{j_1,j_1+1},\dots,R_{j_m,j_m+1}$ with $j_1<\dots<j_m$ , the paper's candidate tour is

\psi' = \varphi\,\alpha_{j_1 j_1+1}\,\alpha_{j_2 j_2+1}\cdots\alpha_{j_m j_m+1}.

Formalization targets

Goal: $\psi'$ solves the bottleneck traveling salesman problem

For $B$ sorted, $f\ge0$ locally integrable, $g=0$ , $\varphi$ ranking the $A$ 's and $T$ a minimum spanning tree as above,

\psi' \text{ is a tour}\quad\text{and}\quad m(\psi')\le m(\psi)\ \text{ for every tour } \psi .

The goal fixes no numerical constant. It asserts both that the construction produces a tour and that the tour is optimal, so it is a statement about the paper's algorithm, not only about the optimal value.

Milestones

Lemma 8 (p. 668): for a fixed $q$ , the number of $i$ with $i\le q<\varphi^{-1}\psi(i)$ equals the number of $j$ with $\varphi^{-1}\psi(j)\le q<j$ .
Lemma 7 (p. 668): for a tour $\psi$ , the graph $G_\psi^*$ — $G_\varphi$ plus the arcs $R_{q,q+1}$ selected by these two conditions — is connected.
Eq. (30) (p. 670): if $R_{q,q+1}$ is an arc of $G_\psi^*$ not in $G_\varphi$ , then $m(\psi)\ge c_{q\varphi(q+1)}$ .
$\varphi$ minimizes $m$ (p. 671): $m(\varphi)\le m(\psi)$ for every permutation $\psi$ .
The value of $m(\psi')$ (p. 671): $m(\psi')$ equals some $c_{j\varphi(j)}$ or the cost $c_{q\varphi(q+1)}$ of an arc of $T$ .
Theorem 6, corrected (p. 671): for a directed graph with nested out-neighbourhoods $\Gamma_1\subseteq\dots\subseteq\Gamma_N=\{1,\dots,N\}$ and $\varphi$ listing them as initial segments, a Hamiltonian circuit exists iff $\varphi(q)\in\Gamma_q$ for all $q$ and the graph $G'_\varphi$ is connected.

Significance

The result gives an exact solution of a bottleneck traveling salesman problem by one minimum spanning tree computation and a fixed sequence of transpositions. Since general bottleneck traveling salesman problems are NP-hard, cases with an exact algorithm are the reference points against which heuristics and approximation results are compared. Theorem 6, an application, characterizes Hamiltonicity for directed graphs whose out-neighbourhoods form a chain, a class on which the general Hamiltonian circuit problem becomes a connectivity test.

The result is proved in the paper; the mission formalizes the proof. To our knowledge none of it has a machine-checked proof. The formalization adds two things to the paper. First, the statements are made explicit: the order in which interchanges are applied, the reading of "spanning tree", the integrability of $f$ . Second, Theorem 6 as printed is false (see below), and the mission states and asks for a proof of the corrected version. Machine-checked statements of $G_\psi^*$ and Lemmas 7–8 are also the shared core of the companion mission on the minimal sum tour.

Difficulty

The obvious argument — every tour must "cross" each gap between consecutive components of $G_\varphi$ , so it pays at least the cheapest crossing — fails because the cost of a crossing is not intrinsic to the gap: a tour may cross between components using arcs that are not of the form $R_{q,q+1}$ , and $m$ looks at one arc at a time, not at a sum. The connection between an arbitrary tour and the spanning trees of $G_\varphi$ goes through the auxiliary graph $G_\psi^*$ and a counting argument (Lemma 8), and the sum-minimizing tree must be shown to be bottleneck-optimal as well. For the upper bound, the transpositions in $\psi'$ cascade along runs of consecutive tree arcs, so $\psi'(i)$ need not be $\varphi(i)$ or $\varphi(i+1)$ ; only the maximum $m(\psi')$ has that form, and showing it needs the monotonicity of $c_{ij}$ in $A_j$ and $B_i$ , which holds because $f\ge0$ and $g=0$ .

Formalization scope

Jobs are Fin (n + 1) (0-based; the paper's job $i$ is index $i-1$ ). $A, B : \text{Fin}(n+1)\to\mathbb R$ with Monotone B. The cost keeps the general two-density form (1); the bottleneck hypotheses are $f\ge0$ everywhere, $g$ identically $0$ , and $f$ locally integrable, so that every interval integral is genuine. Permutations are Equiv.Perm, and $\psi\alpha_{ij}$ is ψ * Equiv.swap i j. $m$ is a Finset.sup' over all jobs, including those that $\psi'$ leaves unchanged. The arc $R_{q,q+1}$ is indexed by q : Fin n.

Explicit readings of the paper's phrases:

"tour": $\psi(s)\ne s$ for every nonempty proper subset $s$ (the empty set is always fixed);
"a minimal set of additional arcs that connect": a connecting set of arcs $R_{q,q+1}$ none of whose proper subsets connects;
"minimum spanning tree … with these new costs": minimum sum of $c_{q\varphi(q+1)}$ over all such trees, not a bottleneck tree;
" $j_1,\dots,j_m$ in increasing order": the interchanges are applied to $\varphi$ in increasing index, lowest first;
" $\psi'$ minimizes $m(\psi')$ ": $\psi'$ is a tour and $m(\psi')\le m(\psi)$ for every tour $\psi$ ;
Theorem 6: the condition $\varphi(q)\in\Gamma_q$ for all $q$ is added, without which sufficiency fails (for $N=3$ , $\Gamma_1=\Gamma_2=\{3\}$ , $\Gamma_3=\{1,2,3\}$ , $\varphi=(3,1,2)$ , $G'_\varphi$ is connected but no Hamiltonian circuit exists); the existence of $\varphi$ is a hypothesis, not a claim.

Not formalized: the remark that the results hold for $f=0$ , $g\ge0$ ; the remark that $\psi'=\psi^*$ when $B_i\ge A_{\varphi(i)}$ ; the $O(N^2)$ operation count.

Trivializing formalizations are ruled out: with a Bochner integral and no integrability hypothesis every cost could collapse to $0$ and every claim would hold; dropping the tour conjunct of the goal would let $\varphi$ itself be "optimal"; and a maximum that ignored the unchanged arcs $c_{j\varphi(j)}$ would make the goal false.

The traveling salesman items already on the platform (metric and symmetric models with tours as visiting orders, e.g. MetricTSP, TSPHeuristics.Shared.TSPModel) describe a different model and are not used. A complete development needs permutation cycle structure (Mathlib's Equiv.Perm.SameCycle), connectivity of finite simple graphs, and interval integrals of nonnegative functions; the lemmas on $G_\psi^*$ and Lemma 8 are reusable for the sum objective. Proofs of any milestone are welcome independently.

Selected references

P. C. Gilmore and R. E. Gomory, Sequencing a one state-variable machine: a solvable case of the traveling salesman problem, Operations Research 12(5) (1964), 655–679. https://doi.org/10.1287/opre.12.5.655
O. Gross, The bottleneck assignment problem, RAND Corporation P-1630, 1959. https://www.rand.org/pubs/papers/P1630.html
P. C. Gilmore, E. L. Lawler and D. B. Shmoys, Well-solved special cases, in E. L. Lawler et al. (eds.), The Traveling Salesman Problem, Wiley, 1985, 87–143. ISBN 978-0-471-90413-7

9 thms3 active usersReviewed

Completed

Combinatorics Operations Research·Captain: mikedeng1

Sequencing Jobs to Minimize Total Weighted Completion Time Subject to Precedence Constraints 2: Near the Optimal Ratio, a Maximum-Weight Initial Set Is ρ-MaximalResearch Paper

Motivation

The single-machine sequencing problem with precedence constraints, written $1\mid\mathrm{prec}\mid\sum w_jC_j$ , asks for an order of $n$ jobs on one machine that respects a given acyclic digraph of precedences and minimizes the weighted sum of completion times. It is NP-hard in general (Lawler 1978; Lenstra and Rinnooy Kan 1978), and much of its structural theory goes through a decomposition due to Sidney (Sidney 1975): find an initial set of jobs of maximum weight-to-processing-time ratio, schedule it first, and recurse on the rest. Sidney's decomposition underlies the series-parallel algorithm of the same report, the 2-approximation algorithms for the general problem, and the vertex-cover view of Chudak–Hochbaum, Correa–Schulz and Ambühl–Mastrolilli.

The decomposition is only usable if a ratio-maximal initial set can be found efficiently. Section 7 of E. L. Lawler's report Sequencing jobs to minimize total weighted completion time subject to precedence constraints (IRIA-LABORIA Rapport de Recherche No. 205, December 1976; journal version in Annals of Discrete Mathematics 2, 1978) gives the polynomial algorithm: a binary search on the ratio, where each trial value is tested by one minimum-cut computation in an auxiliary network. This mission formalizes the correctness of that procedure.

Timeline.

1970: Rhys (Management Science 17) solves the selection problem, the bipartite case of a maximum-weight closed set, by minimum cut.
1975: Sidney introduces the decomposition into ratio-maximal initial sets.
1976: Lawler (this report) reduces the search for a ratio-maximal initial set to $O(\log n + \log w^* + \log p^*)$ minimum-cut computations.
1976: Picard (Management Science 22) treats the maximal closure of a general graph by the same network.

Setting

A finite set $N$ of $n=|N|$ jobs carries an acyclic digraph $G=(N,A)$ ; job $i$ must precede job $j$ when $G$ has a directed path from $i$ to $j$ . Job $j$ has an integer processing time $p_j\ge1$ and an integer weight $w_j$ of either sign.

An initial set of $N$ is a set $I\subseteq N$ that contains, with each of its jobs, every predecessor of that job. The ratio of a nonempty set is

\rho(I)=\frac{\sum_{j\in I}w_j}{\sum_{j\in I}p_j},

and a nonempty initial set $I^*$ is ρ-maximal if $\rho(I^*)\ge\rho(I)$ for every nonempty initial set $I$ . Its ratio $\rho^*$ is the optimal ratio.

For a trial value $\rho$ , the trial weights are $\bar w_j=w_j-\rho p_j$ . A maximum-weight initial set for $\bar w$ is computed in the network $G^*$ : add a source $s$ and a sink $t$ , give the arc $(s,j)$ capacity $\max(0,-w_j)$ , the arc $(j,t)$ capacity $\max(0,w_j)$ , and every arc of $G$ capacity $+\infty$ . An $(s,t)$ cutset is a partition $(S,T)$ of the nodes with $s\in S$ , $t\in T$ , of capacity $c(S,T)=\sum_{i\in S}\sum_{j\in T}c_{ij}$ .

The integer data satisfy $-w^*\le w_j\le w^*$ and $1\le p_j\le p^*$ , and $\varepsilon=1/(np^*)^2$ .

Formalization targets

Goal: the last step of the binary search

If $\rho\le\rho^*\le\rho+\varepsilon$ , then every nonempty initial set $I$ of maximum trial weight,

\sum_{j\in I'}(w_j-\rho p_j)\le\sum_{j\in I}(w_j-\rho p_j)\quad\text{for all initial sets } I',

is ρ-maximal. This is the paper's sentence "At this point the smallest value in the interval is chosen for a trial value ρ. … In either case, the maximum weight initial set I which is determined is ρ-maximal" (pp. 16–17).

Milestones

Finite-capacity cutsets of $G^*$ correspond to initial sets $I=T-\{t\}$ (p. 14).
A finite cutset has capacity $\sum_{j\in N}\max(0,w_j)-\sum_{j\in I}w_j$ (p. 15).
A minimum cutset yields a maximum-weight initial set (p. 15).
Cases 1–3: a maximum-weight set of positive, negative or zero trial weight shows that $\rho$ is too small, too large, or optimal (pp. 15–16).
Every attainable ratio lies in $[-w^*,w^*]$ (p. 16).
Two distinct attainable ratios differ by at least $1/(np^*)^2$ (p. 16).

Significance

The goal is what makes Sidney's decomposition algorithmic: a ρ-maximal initial set can be found by a polynomial number of minimum-cut computations, with the bound $2\log_2 n+\log_2 w^*+2\log_2 p^*+1$ on the number of trial values. Ratio-maximal initial sets are the first step of every Sidney-decomposition-based algorithm for $1\mid\mathrm{prec}\mid\sum w_jC_j$ , and the cut network is the standard reduction of maximum-weight closure to minimum cut, used across open-pit mining, project selection and parametric optimization.

The results are classical and proved in the report. No machine-checked version of the closure–cut correspondence, the ratio-separation bound, or the binary-search correctness is known to exist in Lean or on Prove2Me. The mission produces a reusable formal account of initial sets, the network $G^*$ with infinite capacities, and the parametric test of a ratio.

Difficulty

Each step is short on paper; the difficulty is in the corners the paper does not discuss. The paper's "maximum weight initial set" ranges over all initial sets, and the empty set has weight $0$ . At $\rho=\rho^*$ the empty set is a maximizer and is not ρ-maximal, so the final step needs a nonempty maximizer; and Case 2, read literally over all initial sets, can never occur. The argument at the left end of the interval also needs the separation bound in the right direction: the printed display ends with " $<$ ", while the argument needs " $\ge$ ". Finally, initial sets are closed under predecessors along paths, while a cut only sees single arcs, so the correspondence between finite cuts and initial sets needs the arcs of $G$ to stay inside $N$ .

Formalization scope

Jobs are a Finset N in a type ι; the precedence digraph is a relation G with every arc inside N and no directed cycle, and "must precede" is Relation.TransGen G. Weights and processing times are real in the general statements and integers cast to reals in the integer-data statements. Lean evaluates $\rho(\emptyset)=0/0$ as $0$ ; ρ-maximality and every statement about attainable ratios therefore range over nonempty sets. Capacities take values in WithTop ℝ, with $+\infty=\top$ ; a pair of nodes that is not an arc of $G^*$ has capacity $0$ , and an infinite cut has capacity $\top$ . A cutset is given by its sink side $T\subseteq\{s,t\}\cup N$ .

Added hypotheses and corrected slips, all disclosed in the items:

the goal assumes the maximum-weight initial set $I$ is nonempty (the empty-set corner above);
Cases 2 and 3 maximize over nonempty initial sets;
the separation bound is stated with $\ge$ , against the printed " $<$ ";
the capacity display's first line, printed $\sum_{j\in S}c_{sj}$ , is read as $\sum_{j\in T}c_{sj}$ , as its second line shows;
the interval $[-w^*,w^*]$ and the separation bound are stated for every nonempty subset of $N$ , a slight generalisation.

A trivializing formalization is ruled out: the goal assumes neither Case 1 nor Case 3, nor the separation bound, nor anything about cuts; those appear only as milestones. The running-time statements of §7 and the binary search loop itself are out of scope.

A complete development needs finite sums over finsets, path closure of initial sets, and extended-real arithmetic in WithTop ℝ. The cut network with infinite capacities and the closure correspondence are reusable for any maximum-weight closure problem. Proofs of the milestones, and of the goal from Cases 1 and 3 with the separation bound, are welcome.

Selected references

E. L. Lawler, Sequencing jobs to minimize total weighted completion time subject to precedence constraints, IRIA-LABORIA Rapport de Recherche No. 205, 1976. https://hal.science/hal-04716371v1 ; journal version Annals of Discrete Mathematics 2 (1978) 75–90, https://doi.org/10.1016/S0167-5060(08)70323-6
J. B. Sidney, Decomposition algorithms for single-machine sequencing with precedence relations and deferral costs, Operations Research 23 (1975) 283–298. https://doi.org/10.1287/opre.23.2.283
J. M. W. Rhys, A selection problem of shared fixed costs and network flows, Management Science 17 (1970) 200–207. https://doi.org/10.1287/mnsc.17.3.200
J.-C. Picard, Maximal closure of a graph and applications to combinatorial problems, Management Science 22 (1976) 1268–1272. https://doi.org/10.1287/mnsc.22.11.1268

11 thms3 active usersReviewed

Completed

Combinatorics Operations Research·Captain: mikedeng1

An Introduction to Timetabling 2: When Every Teacher Is Available in at Most Two Periods, Limited Backtracking Finds a Timetable or Correctly Reports That None ExistsResearch Paper

Motivation

School and university timetabling is one of the oldest applications of combinatorial optimization. In the class–teacher model, classes and teachers must be brought together for a prescribed number of lectures, each lecture occupies one period, and nobody can be in two places at once. With no further side constraints the model reduces to edge colouring of a bipartite multigraph and is solved exactly by König's theorem. Real instances, however, come with preassignments (a class and a teacher must meet at a fixed period) and unavailabilities (a teacher or a class cannot be scheduled at some periods). With these, deciding whether a daily timetable exists is NP-complete, as the paper records citing Even, Itai and Shamir (1976).

D. de Werra's invited review An introduction to timetabling (European Journal of Operational Research 19, 1985) surveys this landscape. In its §2.2 it isolates one restricted case that is easy: when every teacher is available during at most two periods, a limited backtracking method finds a timetable or proves that none exists (Proposition 2.4, attributed to [9], Even–Itai–Shamir). The Remark that follows recasts the procedure as a decision method for stable sets of half the vertices in graphs with a perfect matching, which is the 2-satisfiability problem in graph form.

Setting

There are $m$ classes $c_1,\dots,c_m$ , $n$ teachers $t_1,\dots,t_n$ and $p$ periods of one day. After removing the preassigned lectures, $\bar r_{ij}\in\mathbb N$ lectures of class $c_i$ with teacher $t_j$ remain; $\bar b_{ik}\in\{0,1\}$ is $1$ exactly when class $c_i$ is available and not preassigned at period $k$ ; $\bar c_{jk}\in\{0,1\}$ is $1$ exactly when teacher $t_j$ is available and not preassigned at period $k$ . A timetable (a solution of CT4) is a $0/1$ array $\bar x_{ijk}$ with

\sum_{k}\bar x_{ijk}=\bar r_{ij},\qquad \sum_{j}\bar x_{ijk}\le\bar b_{ik},\qquad \sum_{i}\bar x_{ijk}\le\bar c_{jk}.

A possible schedule of $t_j$ is the slice $y_{ik}=\bar x_{ijk}$ of a candidate array that satisfies the constraints involving $t_j$ alone. The conflict graph $G$ has one node per pair (teacher, possible schedule); two nodes are linked when they are different schedules of the same teacher or put the same class in the same period. When each teacher has exactly two schedules, they are written $x_j$ and $\bar x_j$ , and in Lean the nodes are (j, true) and (j, false) of Fin n × Bool.

The limited backtracking works on such a graph. The implications $\mathrm{cl}(S)$ of a set $S$ of chosen nodes form the least set containing $S$ such that whenever $u$ is in it and $u$ is linked to a node $w$ of another teacher, the other node of $w$ 's teacher is in it. A state is either $\mathrm{run}(A)$ , with $A$ the nodes fixed so far, or $\mathrm{fail}$ . From $\mathrm{run}(A)$ , for any teacher not yet fixed and any first choice $b$ of its node:

if $\mathrm{cl}(A\cup\{(j,b)\})$ is independent, the procedure moves there;
otherwise, if $\mathrm{cl}(A\cup\{(j,\lnot b)\})$ is independent, it moves there;
otherwise it fails.

Formalization targets

Goal: correctness of the limited backtracking

For every $n$ and every graph $G$ on $\mathrm{Fin}\,n\times\mathrm{Bool}$ in which $x_j$ and $\bar x_j$ are linked for all $j$ :

\begin{aligned} &\text{(1) the move relation is well founded from } \mathrm{run}(\emptyset);\\ &\text{(2) every reachable } \mathrm{run}(A) \text{ with an unfixed teacher has a move};\\ &\text{(3) a reachable } \mathrm{run}(A) \text{ with all teachers fixed has } A \text{ a set of } n \text{ pairwise non-adjacent nodes};\\ &\text{(4) if } \mathrm{fail} \text{ is reachable, } G \text{ has no set of } n \text{ pairwise non-adjacent nodes.} \end{aligned}

All four clauses range over every run of the nondeterministic procedure.

Milestones

A teacher available in at most $2$ periods has at most $2$ possible schedules.
CT4 has a solution iff its conflict graph has $n$ pairwise non-adjacent nodes.
The implications of chosen nodes lie inside every timetable that contains those nodes.
If $A$ is independent and closed under implications, $G$ has a timetable iff it has one containing $A$ .
In a graph $G=(X,E)$ with a perfect matching $M$ , a stable set has at most $|X|/2$ nodes, and one of exactly $|X|/2$ nodes contains one endpoint of every edge of $M$ .

Significance

Proposition 2.4 identifies a polynomial special case inside a scheduling problem that the paper cites as NP-complete in general (Even–Itai–Shamir [9]). The correctness of the procedure is what makes that special case tractable. Milestones 1 and 2 reduce the timetabling instance to a graph question, and the goal settles the graph question. Milestone 4 is the reason the method needs to undo only the last decision. It is the graph form of the autarky principle of 2-SAT solving: a closed, consistent partial assignment can always be kept. Milestone 5 extends the method from timetables to any graph with a perfect matching.

On the formal side, no machine-checked treatment of this reduction or of the backtracking argument exists on the platform; 2-SAT, unit propagation and autarky have no items there either. The statements are proved in the paper only in prose, and the propagation and autarky arguments are compressed into a few sentences. A formal proof makes the invariants explicit: what is closed, what is independent, and why a contradiction after a reversed decision is global.

Difficulty

Soundness of a successful run is an invariant argument. Soundness of failure is the hard part. The naive argument "both choices for $t_j$ lead to a contradiction, hence no timetable" is wrong in general backtracking, because an earlier decision might be at fault, and full backtracking would revisit it. The proof has to show that an earlier permanent decision never needs revisiting. This requires that the set of fixed nodes is closed under implications and independent, so that no unscheduled teacher is linked to it. This invariant must be maintained through both the keep and the reverse moves. Termination and progress are routine but must be stated: without them the correctness clauses hold for a procedure that never moves. On the CT4 side, the reduction must check that the class constraint $(13)$ with $\bar b_{ik}\in\{0,1\}$ splits exactly into per-teacher availability and pairwise disjointness of schedules.

Formalization scope

Data. $\bar r,\bar b,\bar c$ are taken as data; the preassignments that produce them are not modelled. Indices are Fin m, Fin n, Fin p; $0/1$ variables are Bool.
Schedules. The page's "each teacher has exactly 2 possible schedules" holds only after its normalisation. The milestone states the faithful bound $\le 2$ . The CT4-to-graph equivalence is stated for every instance, so its graph has $\sum_j\#\{\text{schedules of }t_j\}$ nodes rather than $2n$ .
Procedure. The implications are an inductive predicate with no iteration bound. A contradiction is a non-independent set of implications, checked against previously fixed nodes as well. The move relation is an inductive Step with one constructor for each of keep, reverse and fail, so the choice of teacher and of first schedule stays arbitrary.
Not formalized. The $O(n^2)$ running time of Proposition 2.4 and of the Remark has no machine model or constant on the page; termination stands in for it.
Ruled out. A goal with only clauses (3)–(4) would be satisfied by a relation with no moves, and a fixed choice rule would prove a weaker statement. The goal therefore includes termination and progress and quantifies over every run.
Needed infrastructure. Mathlib's SimpleGraph, IsIndepSet, IsNIndepSet, Subgraph.IsPerfectMatching, Relation.ReflTransGen and Acc. The autarky lemma (Milestone 4) and the propagation lemma (Milestone 3) are reusable for any 2-SAT-type development. Proofs of the milestones, and a bridge from the CT4 instance to the abstract graph on Fin n × Bool in the exactly-two-schedules case, are welcome.

Selected references

D. de Werra, An introduction to timetabling, European Journal of Operational Research 19 (1985) 151–162. https://doi.org/10.1016/0377-2217(85)90167-5
S. Even, A. Itai, A. Shamir, On the complexity of timetable and multicommodity flow problems, SIAM Journal on Computing 5 (1976) 691–703. https://doi.org/10.1137/0205048
B. Aspvall, M. F. Plass, R. E. Tarjan, A linear-time algorithm for testing the truth of certain quantified boolean formulas, Information Processing Letters 8 (1979) 121–123. https://doi.org/10.1016/0020-0190(79)90002-4

8 thms3 active usersReviewed

Completed

Combinatorics Operations Research Optimization·Captain: mikedeng1

Sequencing a One State-Variable Machine: A Solvable Case of the Traveling Salesman Problem 1: The Spanning-Tree Interchange Tour ψ* Is a Minimal Cost TourResearch Paper

Motivation

The traveling salesman problem is NP-hard in general, so special cost structures under which it can be solved exactly in polynomial time are of lasting interest in combinatorial optimization and scheduling. One of the earliest and most cited such cases comes from sequencing on a machine whose condition is described by a single real number: a furnace temperature, a knife setting, a fill level. Each job must start at a prescribed state and leaves the machine in another, and changing the state between consecutive jobs costs money or time. Finding the cheapest cyclic order of the jobs is a traveling salesman problem with asymmetric costs.

P. C. Gilmore and R. E. Gomory solved this problem exactly in 1964 (Oper. Res. 12(5), 655–679) with an algorithm of $O(N^2)$ simple steps. Their construction became the standard example of a solvable TSP case: it is the starting point of the survey literature on polynomially solvable TSPs (Gilmore, Lawler and Shmoys 1985; Burkard, Deineko, van Dal, van der Veen and Woeginger 1998), and it appears in the no-wait flow shop literature, where two-machine no-wait scheduling reduces to exactly this cost structure.

Setting

There are $N$ jobs $J_1,\dots,J_N$ . Job $i$ must be started when the state of the machine is $A_i$ and leaves the machine in state $B_i$ ; the jobs are numbered so that $j>i$ implies $B_j\ge B_i$ . Two cost densities $f,g:\mathbb R\to\mathbb R$ satisfy $f(x)+g(x)\ge0$ : raising the state through $x$ costs $f(x)$ per unit, lowering it costs $g(x)$ per unit. The changeover cost of having job $j$ follow job $i$ is

c_{ij}=\begin{cases}\int_{B_i}^{A_j}f(x)\,dx & \text{if } A_j\ge B_i,\\ \int_{A_j}^{B_i}g(x)\,dx & \text{if } B_i>A_j.\end{cases}

A permutation $\psi$ of the jobs assigns to each job $i$ its successor $\psi(i)$ and has cost $c(\psi)=\sum_i c_{i\psi(i)}$ . It is a tour if $\psi(s)\ne s$ for every nonempty proper subset $s$ of the jobs, i.e. if it is a single cycle through all jobs.

A permutation $\varphi$ ranks the $A$ if $j>i$ implies $A_{\varphi(j)}\ge A_{\varphi(i)}$ . The interchange $\alpha_{ij}$ swaps $i$ and $j$ ; applying it to $\psi$ gives $\psi\alpha_{ij}$ (first $\alpha_{ij}$ , then $\psi$ ), which exchanges the successors of $i$ and $j$ , at cost $c_\psi(\alpha_{ij})=c(\psi\alpha_{ij})-c(\psi)$ . The graph $G_\varphi$ links $i$ and $\varphi(i)$ for every $i$ ; a spanning tree of $G_\varphi$ is a minimal set of additional arcs $R_{ij}$ that makes it connected, with cost $\sum c_\varphi(\alpha_{ij})$ . Node $q$ is of type 1 if $B_q\le A_{\varphi(q)}$ and of type 2 otherwise.

Given a minimal cost spanning tree $\tau$ of $G_\varphi$ made of arcs $R_{q,q+1}$ , the tour $\psi^*$ is obtained from $\varphi$ by executing the interchanges $\alpha_{q,q+1}$ , $R_{q,q+1}\in\tau$ , first those of type 1 in decreasing order of $q$ , then those of type 2 in increasing order of $q$ .

Formalization targets

Goal: Theorem 5

\psi^*\ \text{is a tour, and}\quad c(\psi^*)\le c(\psi)\ \text{ for every tour }\psi.

This is the paper's main theorem. It fixes no constant and no special form of $f,g$ ; it asserts that the specific tour produced by the algorithm is optimal among all tours.

Milestones

In the order the proof uses them:

Theorem 1: $c(\varphi)=\min_\psi c(\psi)$ over all permutations.
Eq. (11): under $B_j\ge B_i$ , $A_{\psi(j)}\ge A_{\psi(i)}$ , the cost of $\alpha_{ij}$ is $\int_{[B_i,B_j]\cap[A_{\psi(i)},A_{\psi(j)}]}(f+g)$ .
Lemma 1: an interchange between two different cycles merges them.
Theorem 2: the interchanges of a spanning tree, in any order, turn $\psi$ into a tour.
Lemma 2: some minimal cost spanning tree of $G_\varphi$ uses only arcs $R_{i,i+1}$ .
Lemma 5: adjacent interchanges executed on $\varphi$ in the stated order have additive cost.
Theorem 3: $\psi^*$ is a tour of cost $c(\varphi)+c_\varphi(\tau)$ .
Theorem 4: $c(\psi)\ge c(\varphi)+c^*(\psi)$ for every permutation, with the underestimate $c^*$ of (17).
Lemma 7: for a tour $\psi$ the graph $G_\psi^*$ is connected.
Lemma 8: conditions (22a) and (22b) hold for equally many indices.
Eq. (28): $c^*(\psi)\ge c_\varphi(\tau)$ for every tour $\psi$ .

Off the goal's path: Theorem 7, a minimal tour for $(f,g)$ is minimal for $(f+g,0)$ .

Significance

The theorem shows that a traveling salesman problem whose costs come from a one-dimensional state is solved by three polynomial steps: sorting (an optimal assignment), a minimum spanning tree over $N-1$ candidate arcs, and a prescribed sequence of interchanges. It is the base case for a family of later results on solvable TSPs and for the two-machine no-wait flow shop, where it gives an exact polynomial algorithm.

The result has been proved since 1964. No machine-checked proof of it is known to exist. The proof in the paper argues largely from figures ("evident geometrically"), and its statement of Theorem 3 lists the interchanges in an order that contradicts its own proof: executed in the printed order, the paper's numerical example yields a tour of cost 39 instead of the optimum 34. A formal proof settles which order is correct and fills in the geometric steps. Partial contributions are useful: the permutation facts (Lemmas 1, 8 and Theorem 2) are independent of the cost model and reusable.

Difficulty

The obvious argument fails at two points. First, interchanges do not commute in cost: once one interchange is executed, the cost of the next one depends on the new successors, so the cost of $\psi^*$ is not simply $c(\varphi)$ plus the tree cost for an arbitrary execution order. Showing that the specific order of Lemma 5 avoids all interference requires tracking how type-1 and type-2 nodes behave as interchanges are applied. Second, optimality is not a local statement: an arbitrary tour is not reachable from $\varphi$ by tree interchanges, so the lower bound needs the separate underestimate $c^*$ and a counting argument relating every tour to a spanning tree of $G_\varphi$ . Neither step follows from general minimum spanning tree theory.

Formalization scope

Jobs are Fin (n + 1) ( $N=n+1\ge1$ ), so the paper's job $i$ is index $i-1$ ; the adjacent arc $R_{q,q+1}$ is indexed by q : Fin n and joins q.castSucc and q.succ. Permutations are Equiv.Perm (Fin (n + 1)), and $\psi\alpha_{ij}$ is ψ * Equiv.swap i j (Mathlib's composition, "first $\alpha_{ij}$ , then $\psi$ "). Costs are real; (1) uses oriented interval integrals and (17) set integrals.

Explicit readings of the paper's loose phrases:

"any integrable functions $f,g$ " is read as local integrability on $\mathbb R$ , with $f+g\ge0$ the only sign condition;
"proper subsets $s$ " in (4) are nonempty proper subsets;
"a minimal set of additional arcs that connect" is minimal under inclusion; "minimal cost spanning tree" is minimal in cost among spanning trees made of adjacent arcs (by Lemma 2 the same minimum as over all trees);
"minimal cost tour" means cost at most that of every tour, i.e. every permutation that is a single cycle;
"obtained by executing the $\alpha$ 's in a particular order" (Lemma 5) is the explicit order of its proof;
ties among the $A$ leave $\varphi$ non-unique; every statement holds for every ranking $\varphi$ .

The order of $\psi^*$ is that of the proof of Lemma 5 and of steps T2–T4 (p. 673), not the order printed in Theorem 3.

Trivializing formalizations are ruled out: the goal quantifies over all tours, not over permutations (that is Theorem 1) nor over tours reachable from $\varphi$ ; $\psi^*$ is constructed from $\varphi$ and $\tau$ , not taken as an arbitrary tour of the right cost; $\tau$ is both inclusion-minimal and cost-minimal; and the costs keep both branches of (1) with general densities, not $c_{ij}=|A_j-B_i|$ . The TSP items already on the platform concern symmetric or metric distances with tours as visiting orders, a different model, and are not reused.

Needed infrastructure: cycle structure of permutations under transpositions (Mathlib's Equiv.Perm.SameCycle), connectivity of finite simple graphs, interval integrals of locally integrable functions. Contributions to any milestone are welcome; the purely combinatorial ones (Lemmas 1, 8, Theorem 2, Lemma 7) are independent of the integrals.

Selected references

P. C. Gilmore and R. E. Gomory, Sequencing a one state-variable machine: a solvable case of the traveling salesman problem, Operations Research 12(5), 1964, 655–679. https://doi.org/10.1287/opre.12.5.655
P. C. Gilmore, E. L. Lawler and D. B. Shmoys, Well-solved special cases, in The Traveling Salesman Problem (Lawler, Lenstra, Rinnooy Kan, Shmoys, eds.), Wiley, 1985, 87–143. ISBN 978-0-471-90413-7
R. E. Burkard, V. G. Deineko, R. van Dal, J. A. A. van der Veen and G. J. Woeginger, Well-solvable special cases of the traveling salesman problem: a survey, SIAM Review 40(3), 1998, 496–546. https://doi.org/10.1137/S0036144596297514
J. B. Kruskal, On the shortest spanning subtree of a graph and the traveling salesman problem, Proc. AMS 7(1), 1956, 48–50. https://doi.org/10.1090/S0002-9939-1956-0078686-7

15 thms3 active usersReviewed

Completed

Combinatorics Computational Geometry Discrete Geometry·Captain: mikedeng1

A Combinatorial Theorem in Plane Geometry: Every n-Triangulation Can Be Partitioned into at Most ⌊n/3⌋ FansResearch Paper

Motivation

In a conversation reported by Chvátal, Victor Klee asked for the smallest number $f(n)$ such that every region bounded by a simple closed $n$ -gon is dominated by $f(n)$ points: every point of the region sees one of them along a segment inside the region. In the picturesque language that gave the problem its name, $f(n)$ is the number of guards needed to watch any art gallery with $n$ walls. A comb-shaped polygon (Figure 1 of the paper) shows $f(n) \ge \lfloor n/3 \rfloor$ .

V. Chvátal's three-page note (J. Combin. Theory Ser. B 18 (1975) 39–41) proves the matching upper bound by reducing it to a purely combinatorial statement about triangulated polygons: every such triangulation splits into at most $\lfloor n/3\rfloor$ fans, and a fan is watched by a single guard. The combinatorial theorem is the result this mission formalizes.

Timeline.

1973: Klee poses the question to Chvátal (the paper reports the conversation; the year is O'Rourke's).
1975: Chvátal proves $f(n) = \lfloor n/3\rfloor$ via the fan partition theorem, by induction on $n$ with a four-case analysis.
1978: S. Fisk gives the short proof by 3-colouring the vertices of the triangulation (J. Combin. Theory Ser. B 24 (1978) 374); the smallest colour class is a set of at most $\lfloor n/3\rfloor$ vertices meeting every triangle.
1987 onwards: J. O'Rourke's monograph Art Gallery Theorems and Algorithms (Oxford University Press, 1987) makes the theorem the starting point of a large literature on guarding problems.

Setting

An $n$ -triangulation (p. 39) is a planar graph $G$ with $n$ vertices such that one face is bounded by an $n$ -gon and every other face by a triangle. Its vertices are labelled $0, 1, \dots, n-1$ in their cyclic order around the $n$ -gon, and indices are taken mod $n$ ; the sides of the $n$ -gon are the pairs $\{a, a+1\}$ . Every other edge of $G$ is inner; it is a diagonal $\{a, b\}$ of the $n$ -gon. Two diagonals cross when their endpoints are distinct and alternate around the polygon.

Combinatorially, an $n$ -triangulation requires $n\ge 3$ and is the same thing as a set $D$ of diagonals that pairwise do not cross and is maximal with this property. Its triangles are the 3-element vertex sets all of whose pairs are edges of $G$ ; there are $n - 2$ of them, and they are the bounded faces.

Two triangles are adjacent when they share an edge. A set $F$ of triangles is dual-connected when any two of its members are joined by a chain of adjacent members; such an $F$ is a sub-polygon of $G$ , a $k$ -triangulation with $k = |F| + 2$ , whose inner edges are the edges shared by two of its triangles. Following the paper, a $k$ -triangulation is a fan if one of its vertices, the centre, meets all $k-3$ of its inner edges. A partition of $G$ into fans is a family of fans, pairwise disjoint as sets of triangles, covering all triangles of $G$ . Fans may share vertices and edges.

Formalization targets

Goal: Chvátal's theorem (p. 39)

For every $n \ge 3$ and every $n$ -triangulation $G$ there is a partition of $G$ into $m$ fans with

m \le \left\lfloor \frac{n}{3} \right\rfloor .

Milestones (the claims of the proof, pp. 40–41, in attack order)

Base case. Every $n$ -triangulation with $3 \le n \le 5$ is a fan.
Least span. For $n \ge 6$ , let $k$ be the least integer with $k \ge 4$ such that $G$ has an inner edge $\{j, j+k\}$ . Then $k \le 6$ .
The cut. An inner edge $\{j, j+k\}$ with $2 \le k \le n-2$ cuts $G$ into a $(k+1)$ -triangulation $G_1$ on $j, \dots, j+k$ and an $(n-k+1)$ -triangulation $G_2$ on $j+k, \dots, j$ , whose triangles together are those of $G$ .
The four cases. If $4 \le k \le 6$ and every inner edge $\{a,b\}$ of $G_1$ (relabelled $0,\dots,k$ , $a<b$ ) has $b - a \le 3$ , then $G_1$ is a fan or one of three explicit configurations (cases (2)–(4) of the paper), up to the mirror image $i \mapsto k - i$ .
Tightness. For every $n \ge 3$ some $n$ -triangulation admits no partition into fewer than $\lfloor n/3\rfloor$ fans:

\forall n\ge 3\ \exists G\ \forall P:\quad |P| \ge \lfloor n/3\rfloor .

The goal's only constant is the paper's $\lfloor n/3 \rfloor$ , which milestone 5 shows is best possible.

Significance

The result. The fan partition is a strengthening of the guard bound: the centres of the fans form a set of at most $\lfloor n/3\rfloor$ vertices meeting every triangle, but the partition also says that the triangles split into star-shaped pieces, each visible from one vertex. With the existence of triangulations of simple polygons it yields $f(n) \le \lfloor n/3 \rfloor$ , the art gallery theorem; with Figure 1 it gives $f(n) = \lfloor n/3\rfloor$ .

Formalizing it. The theorem has been proved since 1975, and the platform already has Fisk's consequence: ProofsInTheBook.Chapter36.chapter36 and chapter36_artgallery_combinatorial (Proofs from THE BOOK, Chapter 36) prove that an inductively built family of triangles has a hitting set of at most $n/3$ vertices, and ProofsInTheBook.PolygonGeometryDischarge.artGallery_strict_of_residue proves a geometric guard bound conditional on two assumed inputs. Neither states the fan partition, which is strictly stronger than a hitting set, and neither uses the cyclic labelling of a triangulated polygon. This mission asks for a machine-checked proof of Chvátal's own theorem and of the claims of his proof, on a reusable encoding of triangulated polygons (cyclic labels, non-crossing diagonals, triangles, cutting along a diagonal) that other results on polygon triangulations can build on.

Difficulty

The induction itself is short on paper; the work is in what the paper calls easy. Cutting $G$ along a diagonal and relabelling each piece cyclically must be shown to produce triangulations again, with the triangles split exactly between the two pieces; this is a statement about non-crossing chords that has no counterpart in Mathlib. The case analysis "it is easy to verify that we have one of the following four cases" is an enumeration of all triangulations of a 5-, 6- or 7-gon whose diagonals have span at most 3, and its exhaustiveness (including the mirror images of (2) and (4)) is precisely what the four inductive constructions rely on. The constructions then enlarge one fan of a smaller triangulation, so the induction must be carried out for partitions of arbitrary triangulations, with fans that share edges.

Formalization scope

Encoding of "planar graph". Mathlib has no planar embeddings. An $n$ -triangulation is encoded as the labelled $n$ -cycle on Fin n (vertex $i$ is the paper's $i+1$ ) plus a finset D : Finset (Sym2 (Fin n)) of diagonals that pairwise do not cross and is maximal. Maximality is binding: without it the empty set would "triangulate" every polygon and the goal would hold vacuously.
Triangles are the 3-element vertex sets whose pairs are all edges; in a triangulated polygon every 3-cycle bounds an inner face.
"Partitioned into fans" means a finset of fans, pairwise disjoint as sets of triangles, covering all triangles. A fan must be nonempty, dual-connected, and have a centre on all of its inner edges (edges shared by two of its triangles). Dropping dual-connectedness would turn the goal into Fisk's hitting-set bound; dropping the centre would let the whole triangulation be one "fan". Both clauses are stated.
"[n/3]" is the floor, n / 3 in ℕ. The goal assumes only $n \ge 3$ .
"The least $k \ge 4$ such that $G$ has an edge $(j, j+k)$ " is read over inner edges, with the minimality stated explicitly; read over all edges, a side of span $n-1$ would make the claim trivial for $n = 6, 7$ .
"Cuts $G$ into" is stated for every inner edge of span $2 \le k \le n-2$ (the paper's $4 \le k \le 6$ is a special case), as the pulled-back diagonal sets being triangulations and the triangles splitting between the pieces.
"Mirror image" is the relabelling $i \mapsto k - i$ of $G_1$ (Fin.rev); the four cases are an explicit disjunction on the diagonal set of $G_1$ . The minimality of $k$ enters as the hypothesis that inner edges of $G_1$ have span at most 3.
"Cannot be improved" is stated combinatorially, for the theorem itself; the paper argues it through Figure 1.
Not formalized: Klee's function $f(n)$ , Figure 1's lower bound and the corollary $f(n) \le \lfloor n/3\rfloor$ (p. 41). They need simple polygons in the plane, their interiors, visibility and the existence of triangulations, none of which is available unconditionally.

All definitions are in one file, ChvatalArtGallery.FanPartition.Triangulation; the triangle and cut machinery is reusable for any result on triangulated polygons. Proofs of the milestones, general lemmas on non-crossing diagonal sets (the count $|D| = n-3$ , existence of ears, the dual tree), and alternative proofs of the goal are all welcome.

Selected references

V. Chvátal, A combinatorial theorem in plane geometry, J. Combin. Theory Ser. B 18 (1975) 39–41. https://doi.org/10.1016/0095-8956(75)90061-1
S. Fisk, A short proof of Chvátal's watchman theorem, J. Combin. Theory Ser. B 24 (1978) 374. https://doi.org/10.1016/0095-8956(78)90059-X
J. O'Rourke, Art Gallery Theorems and Algorithms, Oxford University Press, 1987. https://www.science.smith.edu/~jorourke/books/ArtGalleryTheorems/
M. Aigner, G. M. Ziegler, Proofs from THE BOOK, Springer, Chapter "How to guard a museum". https://doi.org/10.1007/978-3-662-57265-8

7 thms3 active usersReviewed

Completed

Combinatorics Operations Research·Captain: mikedeng1

On Representatives of Subsets: Two Partitions into m Classes Have a Common System of Representatives When Any k Classes of One Meet at Least k Classes of the OtherResearch Paper

Motivation

Many assignment questions reduce to one combinatorial question: given finitely many sets, can one choose a different element from each? Workers are matched to jobs they are qualified for, rows of a matrix to columns with nonzero entries. The criterion for when this is possible is Hall's marriage theorem, first stated and proved by P. Hall in a five-page note in 1935 (DOI 10.1112/jlms/s1-10.37.26). It underlies bipartite matching, the integrality of the assignment polytope, the Birkhoff–von Neumann theorem on doubly stochastic matrices, and transversal theory in matroids.

Hall's note was written with a second question in view. In 1916 D. König proved, in the language of bipartite graphs, that if a set of $mn$ things is divided into $m$ classes of $n$ things in two ways, then one can choose $m$ things that represent every class of both divisions at once ("Über Graphen und ihre Anwendungen", Math. Annalen 77 (1916), 453). Van der Waerden (1927) and Sperner (1927) gave the set-theoretic form and a short proof. Hall's contribution was a criterion for a common system of representatives of two divisions in which the classes need not have equal sizes, obtained from the marriage theorem in two short steps.

Setting

Let $S$ be any set, finite or infinite, and let

T_1, T_2, \dots, T_m \tag{1}

be a finite system of subsets of $S$ . The sets $T_i$ may be infinite and need not be distinct; when one speaks of $k$ of the sets, $k$ indices are meant, so a repeated set is counted with multiplicity. A complete set of distinct representatives, or C.D.R., of (1) is a choice of pairwise distinct elements $a_1, \dots, a_m$ of $S$ with

a_i \in T_i \qquad (i = 1, \dots, m).

The system satisfies Hall's condition when any $k$ of the sets contain between them at least $k$ elements of $S$ , for $k = 1, \dots, m$ . The meet of all C.D.R.s, written $R$ , is the set of elements of $S$ that occur as a representative in every C.D.R. of (1).

A division of $S$ into classes is a family of pairwise disjoint sets $S_1, S_2, \dots$ whose union is $S$ . The paper writes $A \wedge B$ and $A \vee B$ for intersection and union; this mission writes $A \cap B$ and $A \cup B$ .

In Lean the system is T : ι → Set α over a finite index type, a C.D.R. is an injective a : ι → α with a i ∈ T i (IsCDR), Hall's condition is HallCondition, and the meet of all C.D.R.s is cdrMeet, all in the namespace HallReps.CDR.

Formalization targets

Goal: Theorem 3 (pp. 29–30)

Let $S$ be divided into $m$ classes in two ways, $S = S_1 \cup \dots \cup S_m = S_1' \cup \dots \cup S_m'$ , each a division into pairwise disjoint classes. If, for each $k$ , any $k$ of the classes $S_j'$ contain between them elements from at least $k$ of the classes $S_i$ , then for some permutation $\sigma$ of $\{1, \dots, m\}$ there are elements

a_i \in S_i \cap S'_{\sigma(i)} \qquad (i = 1, \dots, m).

The set $S$ and the classes may be infinite, and no class is assumed non-empty.

Milestones

Lemma (p. 27). If $a$ is a C.D.R. of (1) and $R$ is the meet of all C.D.R.s, the sets $T_i$ whose representative $a_i$ lies in $R$ contain between them exactly the elements of $R$ , and there are $|R|$ of them.
Induction step, p. 28. With (4) the system $T_1, \dots, T_{m-1}$ and $R^*$ the meet of its C.D.R.s: if $T_m \not\subseteq R^*$ , then (1) has a C.D.R.
Induction step, p. 29. If (4) has a C.D.R. and $T_m \subseteq R^*$ , then some $\rho + 1$ of the sets, including $T_m$ , have union exactly $R^*$ , where $\rho = |R^*|$ .
Theorem 1 (p. 27). Hall's condition is sufficient for a C.D.R. of (1).
Theorem 2 (p. 29). If $S$ is divided into any number of classes and any $k$ of the sets $T_i$ contain between them elements from at least $k$ classes, there are $a_i \in T_i$ lying in pairwise different classes.

A companion item states König's theorem (§1, p. 26), which the paper deduces from Theorem 3 on p. 30.

Significance

Theorem 3 gives a necessary and sufficient criterion for two partitions of a set into $m$ classes to admit a common system of representatives. Necessity is immediate, and the paper proves sufficiency. It contains König's theorem, and through it the statement that a regular bipartite multigraph has a perfect matching, as the case of equal class sizes. Hall remarks that R. Rado's generalization of König's theorem (1933) also follows. Theorem 2, the passage from "distinct elements" to "elements of distinct classes", is the form used for transversals of partitions and is the first instance of what later became the theory of common transversals and matroid intersection.

On the formal side, Hall's theorem for finite sets is in Mathlib as Finset.all_card_le_biUnion_card_iff_existsInjective' (in Mathlib/Combinatorics/Hall/Finite.lean), and the platform already has a proved equivalence for arbitrary sets with a finite index type (YogeshwaranDM.sdr_iff, included in this mission as a reference item) as well as finite bipartite-graph forms. For that reason Theorem 1 is a milestone and not the goal. What this mission adds is Hall's own proof structure, namely the meet of all C.D.R.s and the Lemma about it, which has not been formalized; Theorems 2 and 3 for divisions of a possibly infinite set; and König's theorem in its set-partition form. To our knowledge none of these statements has a machine-checked proof on the platform.

Difficulty

Theorem 3 does not follow from Theorem 1 applied to the classes $S_j'$ directly. Theorem 1 produces distinct elements, but the conclusion needs elements in distinct classes $S_i$ , and two distinct elements of $S_j'$ may lie in the same $S_i$ . The paper's route goes through Theorem 2, which allows any number of classes. That route needs Theorem 1 for systems whose sets can be infinite, because a single $T_i$ may meet infinitely many classes, so the finite-set version of Hall's theorem in Mathlib is not enough on its own. In Hall's own proof of Theorem 1, the work lies in the Lemma. It is an exchange statement about all C.D.R.s at once, whose object $R$ is defined by a universal quantifier over C.D.R.s, and it must be established over an arbitrary finite index type with possibly infinite sets.

Formalization scope

The ground set is a type α, with no finiteness or decidability assumed. The system (1) is T : ι → Set α with [Finite ι] (or Fin (m + 1) in the two induction steps, where the paper's $m$ is the Lean m + 1, its last set is T (Fin.last m), and (4) is fun i : Fin m => T i.castSucc).
Cardinalities of unions of the $T_i$ are Set.encard in ℕ∞, so an infinite union counts as infinite. Set.ncard is used only for subsets of Fin m, for the finite set $R^*$ (with its finiteness stated), and in König's theorem.
" $k$ of the sets" is a Finset ι of indices, so repeated sets count with multiplicity.
Divisions into classes are class maps: cls : α → κ in Theorem 2, with κ arbitrary, and p q : α → Fin m in Theorem 3 and König's theorem. A class map makes the classes cover $S$ and be pairwise disjoint by construction. Empty classes are allowed.
In Theorem 3 the permutation is existential and chosen together with the representatives. $a_i \in S_i \cap S'_{\sigma(i)}$ is p (a i) = i ∧ q (a i) = σ i.
Added or dropped hypotheses: the Lemma assumes a C.D.R. exists, as the page does (without one, cdrMeet is all of α). The first induction step omits the page's C.D.R. of (4), because its hypothesis already implies one. König's theorem adds $0 < n$ , which the page presumes and without which the statement is false.
The trivializing formalizations are ruled out. Typing the $T_i$ as Finset α would reduce Theorem 1 to Mathlib and lose the page's "It is not necessary that the sets $T_i$ shall be finite". Measuring unions by ncard would make Hall's condition fail exactly when a union is infinite. An infinite index type would make Theorem 1 and the Lemma false. None of these is used.
Useful contributions include proofs of the Lemma and of the induction steps, a proof of Theorem 1 either from them or from Mathlib's Hall theorem via a reduction to finite sets, and the reductions Theorem 1 → Theorem 2 → Theorem 3 → König.

Selected references

P. Hall, On representatives of subsets, J. London Math. Soc. 10 (1935), 26–30. https://doi.org/10.1112/jlms/s1-10.37.26
D. König, Über Graphen und ihre Anwendungen auf Determinantentheorie und Mengenlehre, Math. Annalen 77 (1916), 453–465. https://doi.org/10.1007/BF01456961
B. L. van der Waerden, Ein Satz über Klasseneinteilungen von endlichen Mengen, Abh. Math. Sem. Hamburg 5 (1927), 185–188. https://doi.org/10.1007/BF02952519
R. Rado, Bemerkungen zur Kombinatorik im Anschluss an Untersuchungen von Herrn D. König, Sitzungsber. Berliner Math. Ges. 32 (1933), 60–75.
Mathlib, Mathlib/Combinatorics/Hall/Finite.lean and Mathlib/Combinatorics/Hall/Basic.lean. https://github.com/leanprover-community/mathlib4

8 thms3 active usersReviewed

Completed

Combinatorics·Captain: mikedeng1

The Intersection Graphs of Subtrees in Trees Are Exactly the Chordal Graphs: A Finite Graph Is a Subtree Graph If and Only If It Is ChordalResearch Paper

Motivation

Chordal graphs (graphs in which every long cycle has a shortcut edge) appear wherever a sparse symmetric structure has to be eliminated without creating new interactions: Gaussian elimination on sparse symmetric matrices (Rose 1970), acyclic database schemes, junction trees for probabilistic graphical models, and phylogenetic and scheduling problems. In all of these applications the useful object is not the graph itself but a tree representation of it: a tree on which every vertex of the graph is a connected piece, and adjacency is overlap.

The theorem of this mission says that such tree representations exist exactly for chordal graphs. It extends the theory of interval graphs (intersection graphs of intervals on a line, i.e. of subpaths of a path), whose characterization was asked by Hajós (1957) and given by Lekkerkerker–Boland (1962), Gilmore–Hoffman (1964) and Fulkerson–Gross (1965), from paths to arbitrary trees.

Timeline. Dirac (1961) proved that every chordal graph has a simplicial vertex, a vertex whose neighbourhood is a complete subgraph. Rose (1970) used this to recognize chordal graphs efficiently, and Gavril (1972) showed that a chordal graph has at most as many maximal cliques as vertices. Renz (1970) studied intersection graphs of arcs in trees. Gavril (1974), together with Buneman (1974) and Walter (1972/1978) independently, proved that the intersection graphs of subtrees of trees are exactly the chordal graphs, and gave an algorithm that builds such a representation.

Setting

All graphs are finite and simple: a graph $G$ has a finite vertex set $V$ and a symmetric irreflexive adjacency relation. A completely connected set is a set of pairwise adjacent vertices, and a clique is a maximal completely connected set. The set of cliques of $G$ is $\mu(G)$ , and $\mu_v(G) \subseteq \mu(G)$ is the set of cliques containing the vertex $v$ . For a vertex $v$ , $\Gamma v$ is the set of its neighbours; $v$ is simplicial if $\Gamma v$ is completely connected.

$G$ is chordal if every simple circuit $v_1, \dots, v_k, v_1$ with $k > 3$ vertices has a chord: an edge of $G$ joining two vertices of the circuit that are not consecutive on it.

A tree $T$ is a connected graph without simple circuits. A subtree of $T$ is a nonempty set of tree vertices that induces a connected subgraph of $T$ . A family $(\bar v)_{v \in V}$ of subtrees of $T$ represents $G$ if, for all distinct $u, v \in V$ ,

u \sim_G v \iff \bar u \cap \bar v \neq \varnothing.

$G$ is a subtree graph if it has such a representation on some tree, and a proper subtree graph if it has one in which no subtree is contained in another.

Formalization targets

Goal: Theorem 3 (p. 51)

G \text{ is a subtree graph} \iff G \text{ is chordal}

for every finite simple graph $G$ . The paper calls this "the main theorem of this paper".

Milestones

The three-point remark (p. 50): subtrees of a tree that each contain two of three given points have a common point.
Lemma 1 (p. 50): for every completely connected set $A$ of a subtree graph, $\bigcap_{v \in A} \bar v \neq \varnothing$ .
For two different cliques $A_1 \neq A_2$ , $\big(\bigcap_{v\in A_1}\bar v\big) \cap \big(\bigcap_{v \in A_2} \bar v\big) = \varnothing$ (p. 50).
Theorem 2 (p. 51): $G$ is a subtree graph if and only if there is a tree $T$ with vertex set $\mu(G)$ such that $T(\mu_v(G))$ is connected for every $v \in V$ (a clique tree).
Subtree graphs are chordal (proof of Theorem 3, p. 51).
Dirac–Rose (cited, p. 48): every nonempty finite chordal graph has a simplicial vertex.
For a simplicial vertex $v$ , $\{v\} \cup \Gamma v$ is a clique (p. 52).
Induced subgraphs of chordal graphs are chordal (p. 52).
Every finite chordal graph has a clique tree (pp. 51–52).

Companion statements (§3 and §1)

G \text{ subtree graph} \implies G \text{ proper subtree graph}, \qquad \text{subtree} \iff \text{proper subtree} \iff \text{chordal},

and, cited on p. 49, $|\mu(G)| \le |V|$ for a nonempty finite chordal graph.

Significance

The result. The theorem turns a forbidden-structure condition (no chordless cycle of length at least four) into a constructive geometric one (a tree model), and Theorem 2 makes the tree canonical: its vertices are the maximal cliques. Clique trees are the data structure behind junction-tree inference, multifrontal sparse Cholesky factorization, and dynamic programming over tree decompositions; the treewidth of a graph is defined through chordal supergraphs and their clique trees. The proper-subtree result of §3 shows a contrast with interval graphs, where proper interval graphs form a strictly smaller class.

Formalizing it. The theorem is classical and fully proved in the literature, but Mathlib has no notion of chordal graph, no Helly property for subtrees, no clique trees and no simplicial-vertex theorem. This mission produces those definitions together with the characterization, the Helly property for finite families of subtrees, the Dirac–Rose theorem under the cycle–chord definition, and closure of chordality under induced subgraphs. As far as is known, none of these results has a machine-checked proof in Lean under the cycle–chord definition.

Difficulty

The "only if" direction is short on paper but rests on tree facts that are not packaged in Mathlib: a connected vertex set of a tree contains the unique path between any two of its vertices, and three pairwise paths of a tree meet. The "if" direction must produce a tree on the set $\mu(G)$ of maximal cliques, and the maximal cliques of a graph are not stable under passing to induced subgraphs: a clique of a subgraph need not be a clique of $G$ , and two cliques of $G$ may restrict to the same set. Relating $\mu(G)$ to $\mu(G_1)$ for a smaller graph $G_1$ is the step where informal arguments are routinely loose, and it is where a formal proof spends most of its effort. The Dirac–Rose theorem is cited rather than proved in the paper and needs a separate development.

A tempting shortcut is to define chordality as the existence of a perfect elimination ordering. This builds the Dirac–Rose theorem into the definition and changes the theorem being proved; it is excluded here.

Formalization scope

Graphs are G : SimpleGraph V with [Fintype V] in the goal, Theorem 2, the clique-tree claim, Dirac–Rose and the clique count. Milestones whose claims hold for infinite graphs (Lemma 1 for finite $A$ , the three-point remark, the clique-disjointness claim, subtree ⇒ chordal, induced chordality, the simplicial clique, subtree ⇒ proper subtree) are stated without finiteness, which makes them stronger. $V$ may be empty in the goal and in Theorem 2; Dirac–Rose and the clique count assume $V$ nonempty, which they need.
Chordality is the cycle–chord definition: for every cycle walk c of length at least 4 there are vertices x, y on c with G.Adj x y and s(x, y) not an edge of c.
The paper's trees are topological and its subtrees connected closed portions that may end inside an edge. Here a tree is a combinatorial tree T : SimpleGraph β with T.IsTree (not necessarily finite), and a subtree is a vertex set s with (T.induce s).Connected; subdividing the topological tree at all end-points shows the class of subtree graphs is the same. The tree type lives in the same universe as V.
The representing family is indexed by V; adjacency is compared only for distinct vertices. A clique is Maximal G.IsClique s; $\mu(G)$ is the subtype of such sets.
Two trivializing formalizations are ruled out: chordality as a perfect elimination ordering, and representations by sets that need not be connected (with arbitrary sets every graph is an intersection graph, and the "only if" half would be false).
Needed infrastructure: paths and connected sets in trees, Helly's property for subtrees, maximal cliques and their behaviour under induced subgraphs, and simplicial vertices. The tree lemmas and the Dirac–Rose theorem are reusable well beyond this mission. Proofs of any milestone, alternative routes (for example via perfect elimination orderings proved equivalent to the cycle–chord definition), and the clique-count bound are all welcome.

Selected references

F. Gavril, Algorithms for minimum coloring, maximum clique, minimum covering by cliques, and maximum independent set of a chordal graph, SIAM J. Comput. 1 (1972) 180–187. https://doi.org/10.1137/0201013
F. Gavril, The intersection graphs of subtrees in trees are exactly the chordal graphs, J. Combin. Theory Ser. B 16 (1974) 47–56. https://doi.org/10.1016/0095-8956(74)90094-X
G. A. Dirac, On rigid circuit graphs, Abh. Math. Sem. Univ. Hamburg 25 (1961) 71–76. https://doi.org/10.1007/BF02992776
D. J. Rose, Triangulated graphs and the elimination process, J. Math. Anal. Appl. 32 (1970) 597–609. https://doi.org/10.1016/0022-247X(70)90282-9
P. Buneman, A characterisation of rigid circuit graphs, Discrete Math. 9 (1974) 205–212. https://doi.org/10.1016/0012-365X(74)90002-8
J. R. Walter, Representations of chordal graphs as subtrees of a tree, J. Graph Theory 2 (1978) 265–267. https://doi.org/10.1002/jgt.3190020311
D. R. Fulkerson and O. A. Gross, Incidence matrices and interval graphs, Pacific J. Math. 15 (1965) 835–855. https://doi.org/10.2140/pjm.1965.15.835

11 thms3 active usersReviewed

Completed

Linear Optimization Operations Research·Captain: mikedeng1

A Suggested Computation for Maximal Multi-Commodity Network Flows: With Nonnegative Simplex Multipliers, Shortest-Chain Labels Prove the Arc-Chain Basis Optimal or Find an Entering ChainResearch Paper

Motivation

The maximal multi-commodity flow problem asks how much total flow several commodities, each travelling from its own sources to its own sinks, can send through a network whose arcs have shared capacities. It arises in communication and transportation planning: Kalaba and Juncosa's 1956 study of communication networks (Management Science 3(1)) leads to linear programs of this form. For a single commodity the problem has a clean combinatorial theory: the max-flow min-cut theorem of Ford and Fulkerson (1956, doi:10.4153/CJM-1956-045-5) and the labeling algorithm. With several commodities both fail: the min-cut equality is false, and simplex bases are no longer triangular.

In a short note received in October 1957 and published in Management Science in 1958, L. R. Ford Jr. and D. R. Fulkerson proposed a way to solve the multi-commodity problem with the simplex method anyway (doi:10.1287/mnsc.1040.0269, reprinted 2004). They use the arc-chain formulation, which has one variable per chain from a source to a sink of a commodity. That formulation has far too many variables to write down. The note's point is that the simplex method never needs them explicitly. The "pricing" step (finding a variable to enter the basis, or recognizing that none exists) can be carried out by one shortest-chain computation per commodity, with the simplex multipliers as arc lengths.

Timeline. Ford (1956, RAND P-923) gave the label-correcting shortest-chain procedure the note uses. Ford and Fulkerson (1958) applied it to price the columns of the arc-chain program. Dantzig and Wolfe (1960) generalized the idea into the decomposition principle. Gilmore and Gomory (1961) applied the same pattern to the cutting-stock problem, and it is now called column generation.

Setting

A network has finitely many nodes $P_1,\dots,P_N$ and arcs $A_1,\dots,A_m$ . Each arc $A_r$ joins two nodes, has a capacity $b_r$ , and is either directed (traversable one way only) or undirected (traversable both ways). There are finitely many commodities; commodity $k$ has a set of sources $S_k$ and a set of sinks $T_k$ .

A chain from $u$ to $w$ is the arc set of a path $u = v_0, v_1, \dots, v_p = w$ with distinct nodes, each arc traversable from $v_{i-1}$ to $v_i$ . A commodity chain of $k$ is a chain from a node of $S_k$ to a node of $T_k$ . List the commodity chains, for all commodities, as $C_1,\dots,C_n$ , and let $A = (a_{rs})$ be the incidence matrix: $a_{rs} = 1$ if $C_s$ contains $A_r$ and $0$ otherwise. With $x_s$ the flow along $C_s$ and $x_{n+r}$ the slack of arc $A_r$ , the problem is the linear program

\text{maximize } \sum_{s=1}^{n} x_s \quad\text{subject to}\quad \sum_{s=1}^{n} a_{rs}x_s + x_{n+r} = b_r,\qquad x_1,\dots,x_{n+m} \ge 0. \tag{2–3}

A basis is a set of $m$ columns of $[A \mid I]$ forming an invertible matrix $B = (b_{rj})$ . Its simplex multipliers $\alpha_1,\dots,\alpha_m$ satisfy, for every basic column $j$ ,

\sum_{r=1}^{m} \alpha_r b_{rj} = \begin{cases} 1 & j \le n,\\ 0 & j > n.\end{cases} \tag{4}

Read as arc lengths, the $\alpha_r$ give each chain $C_s$ the length $\sum_r \alpha_r a_{rs}$ . The labeling process for a source set $S$ starts with labels $\pi_i = 0$ on $S$ and $\pi_i = \infty$ elsewhere. It repeatedly finds an arc traversable from $P_i$ to $P_j$ with $\pi_i + l_{ij} < \pi_j$ and replaces $\pi_j$ by $\pi_i + l_{ij}$ . In Lean the labels are lab : V → WithTop ℝ, the multipliers are α : E → ℝ, and all objects live in the namespace FordFulkerson58.ArcChain.

Formalization targets

Goal: the shortest-chain pricing test (§3, pp. 1779–1780)

Let $B$ be a basis with basic feasible solution $z$ and multipliers $\alpha \ge 0$ . Then:

\begin{aligned} &\text{(a) for every commodity, every run of the labeling process with lengths } \alpha \text{ is finite;}\\ &\text{(b) if all final sink labels are } \ge 1, \text{ then } \textstyle\sum_s x_s \le \sum_s z_s \text{ for every feasible } x;\\ &\text{(c) if a final sink label } \pi_t < 1, \text{ some non-basic chain column to } t \text{ has length } \pi_t \text{ and } 1 - \textstyle\sum_r \alpha_r a_{rs} > 0. \end{aligned}

Milestones (§3, the labeling process and the test)

Termination of the labeling process for non-negative lengths (p. 1780).
Final labels are shortest-chain lengths from $S$ ; the smallest label on $T$ is the $S$ -to- $T$ distance (p. 1780).
The trace-back: a chain of tight arcs from $S$ to every labeled node, of length its label (p. 1780).
If $\alpha \ge 0$ and every commodity chain has length $\ge 1$ , the basis is optimal (p. 1779).

Further items state the remarks of §3–§4: a negative multiplier lets a slack enter; the slack basis is a feasible start; dominated chains can be ignored; limited supplies reduce to the same problem by adding new directed source arcs; Figure 2 is the incidence matrix of Figure 1; with negative lengths the labeling process may not terminate.

Significance

The result. The test turns a linear program with exponentially many columns into one whose pricing step costs one shortest-path computation per commodity. Only the $m \times m$ basis is ever stored. This is the first instance of column generation, which now underlies solvers for multi-commodity flow, cutting stock, vehicle routing, crew scheduling and many other set-partitioning models, typically inside branch-and-price. Part (a) together with milestones 2–3 also gives the correctness of Ford's label-correcting algorithm with non-negative lengths, started from a source set and with any order of arc scans.

Formalizing it. The results are classical and proved in the paper's informal style. None of them is formalized: the platform has no arc-chain LP, no column pricing, and no formal statement of Ford's label-correcting process. The general LP facts are on the platform (the simplex optimality criterion and weak duality, both proved) and are included as references. This mission adds the network-specific layer: chains as arc sets of simple paths, the labeling process as a relation on labelings, and the link from final labels to reduced costs. One sentence of the paper is corrected. The trace-back "eventually" reaches $S$ only along some backward path, because zero-length cycles can trap a naive backward search, and milestone 3 states the true version.

Difficulty

The obvious argument for termination says each step lowers a label and there are finitely many chains. It fails: labels are lengths of walks, not chains, and with zero-length arcs (multipliers are often $0$ ) there are infinitely many walks. Termination needs the finiteness of the set of walk lengths below a bound, not positivity. The correctness of the final labels needs both properties of the labeling: it is produced by the process (so every label is the length of a walk from $S$ ), and it is terminal. A terminal labeling alone, such as all labels $0$ , is not a distance labeling. Finally, the optimality claim is an LP statement about the full, never-enumerated column set. It must be derived from (4), $\alpha \ge 0$ and the shortest-chain lengths, with the chain columns indexed abstractly.

Formalization scope

Nodes, arcs and commodities are finite types V, E, ι. Each arc has tail, head, a per-arc directed flag and a capacity b : E → ℝ; commodities have src snk : ι → Finset V. Parallel arcs and mixed directed/undirected networks are allowed. No sign of the capacities and no disjointness of sources and sinks is assumed, except 0 ≤ b in the zero-flow item, where it is disclosed. Chains are arc sets of simple paths. The null chain at a source is a chain, so sources have distance $0$ . Columns are pairs (commodity, chain), so one arc set used by two commodities gives two columns. The columns of $[A \mid I]$ are indexed by Col N ⊕ E. A basis is β : E → Col N ⊕ E with IsUnit (basisMatrix N β).det; its basic feasible solution and multipliers (4) are hypotheses about this β. Labels are in WithTop ℝ with ⊤ for $\infty$ . Shortest-chain lengths are finite infima (Finset.inf), equal to ⊤ when there is no chain. The process scans arcs, not node pairs, which handles parallel arcs and the undirected case $l_{ij} = l_{ji}$ .

The standing assumption of §3 ("a stage has been reached in the computation where all $\alpha_r$ are non-negative", p. 1779) is a hypothesis of the goal and of milestones 1–4. Milestones 1–3 are stated for any non-negative length function. The paper has no numbered theorems; every milestone is an unnumbered sentence of §3, cited by page and position.

A trivializing formalization is ruled out: the goal does not assume shortest-chain lengths, the trace-back, or any reduced-cost fact beyond (4). Statements about final labels require labelings that are both reachable from the initial labels and terminal, and part (a) shows such labelings exist.

Reusable beyond this mission: the chain and labeling layer (a label-correcting shortest-path algorithm from a source set over mixed networks) and the arc-chain LP. Contributions to the LP layer, which can import the referenced Matoušek–Gärtner results after reindexing, are particularly welcome.

Selected references

L. R. Ford Jr., D. R. Fulkerson, A suggested computation for maximal multi-commodity network flows, Management Science 5(1):97–101, 1958; reprinted Management Science 50(12S):1778–1780, 2004. https://doi.org/10.1287/mnsc.1040.0269
L. R. Ford Jr., D. R. Fulkerson, Maximal flow through a network, Canadian Journal of Mathematics 8:399–404, 1956. https://doi.org/10.4153/CJM-1956-045-5
L. R. Ford Jr., Network Flow Theory, RAND Corporation Paper P-923, 1956. https://www.rand.org/pubs/papers/P923.html
G. B. Dantzig, P. Wolfe, Decomposition principle for linear programs, Operations Research 8(1):101–111, 1960. https://doi.org/10.1287/opre.8.1.101
P. C. Gilmore, R. E. Gomory, A linear programming approach to the cutting-stock problem, Operations Research 9(6):849–859, 1961. https://doi.org/10.1287/opre.9.6.849
J. Matoušek, B. Gärtner, Understanding and Using Linear Programming, Springer, 2007. https://doi.org/10.1007/978-3-540-30717-4

12 thms3 active usersReviewed

Completed

Combinatorics Operations Research·Captain: mikedeng1

Matching, Euler Tours and the Chinese Postman IV: Every Connected, Even, Symmetric Mixed Graph Has an Euler TourResearch Paper

Motivation

A postman, a snowplough or a street sweeper must traverse every street of a district and return to the depot. When some streets are one-way, the street network is a mixed graph: some edges are directed and must be traversed in a prescribed direction, the others are undirected and may be traversed either way. The first question about such a route is whether a closed route exists that traverses every street exactly once, an Euler tour of the mixed graph. When one exists, it is an optimal postman route; when none exists, the postman problem asks which streets to repeat.

J. Edmonds and E.L. Johnson treat this question in §6 of Matching, Euler tours and the Chinese postman (Mathematical Programming 5, 1973), the paper that solved the undirected Chinese postman problem by matching. Section 6 gives an algorithm that finds an Euler tour in any mixed graph that is connected, of even degree and symmetric, and §7 uses it for the mixed postman problem.

Timeline.

1736: Euler's condition for undirected graphs (even degrees, connectivity).
1951: T. van Aardenne-Ehrenfest and N.G. de Bruijn enumerate the Euler tours of a symmetric directed graph through spanning arborescences ("circuits and trees in oriented linear graphs"). Edmonds and Johnson cite this as the source of their arborescence rule.
1962: L.R. Ford and D.R. Fulkerson (Flows in Networks, §II.7) characterize, by a flow argument, when a mixed graph has an Euler tour without assuming symmetry.
1973: Edmonds and Johnson give the combined orientation and Rule algorithm of §6 for connected, even, symmetric mixed graphs, and the existence criterion of §7 for mixed postman tours.
1976: C.H. Papadimitriou shows the mixed postman problem NP-hard, so the polynomial-time picture of §6 does not extend to its optimization version.

Setting

A mixed graph $G$ has a finite set $N$ of nodes and a finite set $E$ of edges. Each edge $e$ meets two distinct nodes; several edges may meet the same pair of nodes. Some edges are directed: an edge directed away from node $i$ toward node $j$ must be traversed from $i$ to $j$ . In Lean an edge has a tail, a head (distinct) and a Boolean directed; for an undirected edge the order of the two ends carries no meaning.

The degree of a node is the total number of edges, regardless of direction, meeting it. $G$ is even if every degree is even.
$\operatorname{out}(n)$ and $\operatorname{in}(n)$ count the directed edges directed away from and toward $n$ . $G$ is symmetric if $\operatorname{out}(n)=\operatorname{in}(n)$ for every node $n$ .
$G$ is connected if it is connected when the directions on the edges are ignored.
A mixed walk is a sequence $(n_1,e_1,n_2,\dots,e_l,n_{l+1})$ in which each directed $e_i$ goes from its tail $n_i$ to its head $n_{i+1}$ and each undirected $e_i$ meets $n_i$ and $n_{i+1}$ . It is a tour if $n_{l+1}=n_1$ , an Euler tour if it contains every edge exactly once, and a postman tour if it contains every edge at least once.
An arborescence with root $r$ is a tree $T$ of directed edges in which every node $n\neq r$ of $T$ has precisely one edge of $T$ directed away from $n$ . Following those edges from any node of $T$ leads to $r$ . It is spanning if it contains every node.

Formalization targets

Goal: the mixed Euler tour theorem (§6, pp. 115–118)

If $G$ is connected, even and symmetric, then for every node $r$

\exists\ (r=n_1,e_1,\dots,e_l,n_{l+1}=r)\ \text{a mixed Euler tour of } G .

Milestones

Cut balance (p. 116). If $G$ is symmetric, every node set $S$ has as many directed edges leaving it as entering it.
Maximal arborescences span (pp. 115–116). Suppose the directed edges form a symmetric, connected spanning subgraph. Then an arborescence of directed edges to which no directed edge entering it from outside can be added contains every node.
The Rule (pp. 116–117). Suppose the directed edges form a symmetric connected spanning subgraph and the undirected edges have even degree. Fix a spanning arborescence with root $r$ and order the directed edges leaving each node $n\neq r$ so that the arborescence edge comes last. Then the following traversal from $r$ is an Euler tour: leave by the next unused undirected edge if there is one, otherwise by the next unused directed edge.
The assignment outcome (p. 118). If $G$ is connected, even and symmetric, directions can be assigned to some undirected edges so that the result is symmetric, its directed edges form a connected spanning subgraph, and the unassigned edges have even degree.
Mixed postman criterion (§7, p. 120). A connected mixed graph has a postman tour if and only if no nonempty proper node set $S$ has every boundary edge directed away from $S$ .

Significance

The goal contains two classical theorems as special cases. With every edge undirected it is Euler's theorem for connected even multigraphs. With every edge directed it is the theorem that a connected balanced digraph is Eulerian. The milestones connect the two cases: an orientation reduces the mixed case to one the Rule can handle. The Rule itself is the van Aardenne-Ehrenfest–de Bruijn construction, which underlies the BEST theorem counting Euler tours. Milestone 5 decides whether the mixed postman problem has any feasible solution. The mixed postman problem is the standard model for routing on one-way street networks.

All results here are proved in the paper, so none is open. No Lean proof of any of them in this form is known. Mathlib's Eulerian walks are for simple graphs; it has no multigraph or mixed-graph Euler theorem, no directed Euler theorem and no arborescence-based traversal. The mission produces these, together with a reusable vocabulary of mixed multigraphs, walks that respect directions, and arborescences given by parent edges.

Difficulty

The obvious approach to the goal is to forget the directions and apply Euler's theorem. This fails because the tour it produces may traverse a directed edge backwards. Orienting all undirected edges at once also fails: an arbitrary orientation of the undirected edges need not keep every node balanced.

The difficult part of the Rule is showing that the greedy traversal does not get stuck before using every edge. It cannot stop at a node other than $r$ because of the degree conditions. The hard step is showing that no edge is left unused when it stops at $r$ . The answer depends on the ordering condition: without the arborescence edge last at every node, the Rule can return to $r$ with edges still unused. The assignment step needs an invariant: the orientation must keep every node symmetric while it extends a spanning structure of directed edges.

Formalization scope

Graphs. Nodes and edges are finite types (Fintype V, Fintype E). Parallel edges are allowed, including a directed and an undirected edge on the same pair. Loops are excluded (tail e ≠ head e), following the paper's standing setting of §2 (p. 91: edges meet two different nodes). Edges are a type, not a relation on nodes, so parallel edges stay distinct in every walk.
Hypotheses as on p. 115. "Even" counts all edges, directed or undirected. "Symmetric" counts only directed edges. "Connected" ignores directions. Strong connectivity is not assumed. "Symmetric" does not mean that every node has even in-degree, and an Euler tour of the underlying undirected multigraph does not satisfy the goal: the tour must traverse each directed edge from its tail to its head.
Walks are a node list and an edge list of length one less. The one-node walk is allowed, so the graph with one node and no edges satisfies the goal.
Arborescences are given by an optional edge $a_n$ at each node, with an edge required for each non-root node of $W$ ; following those edges leads to $r$ . A maximal arborescence is one where no directed edge enters $W$ from outside. The optional choice represents the root-only arborescence when the graph has no edges.
The Rule is computed by a fuel-bounded traversal (at most $|E|$ steps) that keeps a global list of used edges. Its conclusion is that the computed sequences form a mixed Euler tour from $r$ .
The assignment is an existential statement over a second mixed graph $G'$ on the same edges, with the same unordered ends and every directed edge kept. The paper's algorithm (Steps 0–3) is not formalized.
Postman criterion. "Proper subset" means nonempty and proper. Connectivity is assumed, as throughout §7, and the node set is nonempty (with no nodes there is no tour, while the criterion holds vacuously).
Not formalized. The §7 evenness argument (p. 122) and the min-cost flow formulations are outside the scope.

Contributions are welcome at every level: proofs of the milestones, a direct proof of the goal, and general lemmas about mixed multigraph walks.

Selected references

J. Edmonds and E.L. Johnson, Matching, Euler tours and the Chinese postman, Mathematical Programming 5 (1973) 88–124. https://doi.org/10.1007/BF01580113
T. van Aardenne-Ehrenfest and N.G. de Bruijn, Circuits and trees in oriented linear graphs, Simon Stevin 28 (1951) 203–217.
L.R. Ford and D.R. Fulkerson, Flows in Networks, Princeton University Press, 1962.
C.H. Papadimitriou, On the complexity of edge traversing, Journal of the ACM 23 (1976) 544–554. https://doi.org/10.1145/321958.321974

7 thms3 active usersReviewed

Completed

Combinatorics Operations Research·Captain: mikedeng1

Paths, Trees, and Flowers I: Matching-Duality Theorem — the Maximum Cardinality of a Matching Equals the Minimum Capacity-Sum of an Odd-Set CoverResearch Paper

Motivation

A matching in a graph is a set of edges no two of which share a vertex. Finding a matching of maximum cardinality is one of the basic problems of combinatorial optimization: it models pairing tasks (workers to shifts, kidney donors to recipients, players to rounds), it is a subroutine of algorithms for the travelling salesman and Chinese postman problems, and it was the first problem shown to need more than linear programming over the obvious constraints to be solved exactly.

For bipartite graphs, König's theorem (1931) gives a min–max formula: the maximum size of a matching equals the minimum size of a set of vertices meeting every edge. In general graphs this fails already for a triangle, where a single edge is a maximum matching but two vertices are needed to meet all three edges. Jack Edmonds' paper Paths, trees, and flowers (1965) gave both a polynomial-time algorithm for maximum matching in general graphs, the blossom algorithm, and, as a by-product of its analysis, the correct min–max theorem for general graphs.

Timeline.

1891: Petersen uses alternating paths to prove the existence of factors in certain graphs.
1947: Tutte characterizes graphs with a perfect matching.
1957: Berge proves that a matching is maximum if and only if there is no augmenting path, and derives the deficiency formula now called the Tutte–Berge formula (Berge 1957).
1965: Edmonds shrinks odd circuits ("blossoms") to search for augmenting paths in polynomial time and proves the matching-duality theorem in terms of odd-set covers (Edmonds 1965); the companion paper on the matching polyhedron extends this to weighted matching.

Setting

A graph $G$ is a finite set of vertices and a finite set of edges, each edge meeting exactly two distinct vertices, its end-points. Several edges may join the same two vertices; this is needed because shrinking creates parallel edges. A matching $M$ is a set of edges no two of which meet the same vertex; a vertex is exposed if it meets no edge of $M$ . "Maximum" refers to cardinality.

An odd set is a set $U$ of vertices with an odd number of elements. Its capacity is

\operatorname{cap}(U) = \begin{cases} 1 & |U| = 1,\\ k & |U| = 2k+1,\ k \ge 1.\end{cases}

A one-vertex set covers the edges meeting its vertex; a set of $2k+1 \ge 3$ vertices covers the edges with both end-points in it. An odd-set cover is a family $\mathcal S$ of odd sets such that every edge is covered by some member, and its capacity-sum is $\operatorname{cap}(\mathcal S) = \sum_{U \in \mathcal S} \operatorname{cap}(U)$ .

The proof uses the following objects of §3–§4 of the paper. An alternating path is a simple path whose edges alternate between $M$ and the non-matching edges $\bar M$ . An alternating tree is a tree whose vertices are split into inner and outer vertices, every edge joining an inner to an outer vertex and every inner vertex meeting exactly two tree edges; it is planted if $M$ restricted to the tree is a maximum matching of the tree whose one exposed vertex (the root) is exposed in $G$ , and Hungarian if its outer vertices are adjacent only to its inner vertices. A blossom is an odd circuit on which $M$ is a maximum matching, leaving one vertex $b$ exposed; with a stem (an alternating path from an exposed vertex ending in a matching edge at $b$ ) it forms a flower. Shrinking a vertex set $U$ replaces it by a single vertex $U/U$ , deletes the edges inside $U$ and keeps all other edges; $G/B$ and $M/B = M \cap (G/B)$ denote the result for a blossom $B$ .

Formalization targets

Goal: the matching-duality theorem (5.6, p. 462)

\max\{|M| : M \text{ a matching of } G\} \;=\; \min\{\operatorname{cap}(\mathcal S) : \mathcal S \text{ an odd-set cover of } G\}.

It is stated as: there are a maximum matching $M$ and a minimum odd-set cover $\mathcal S$ with $|M| = \operatorname{cap}(\mathcal S)$ .

Milestones (attack order)

Weak duality: $|M| \le \operatorname{cap}(\mathcal S)$ for every matching and odd-set cover.
3.7 (Berge): $M$ is not maximum iff an alternating path joins two exposed vertices.
4.1–4.2: maximum matchings of an alternating tree.
4.14 and 4.15: the two directions of 4.12, in stronger form.
4.12: for the blossom $B$ of a flower, $M$ is maximum in $G$ iff $M/B$ is maximum in $G/B$ .
4.17: removing a Hungarian tree preserves maximality.
5.7: the theorem for graphs with at most one exposed vertex.
5.8: the configuration produced by the algorithm on a maximum matching, and the odd sets $\mathcal S_J$ it yields, which reduce the theorem to a graph with one exposed vertex fewer.

Significance

The matching-duality theorem gives a certificate of optimality: a matching and an odd-set cover of equal size prove each other optimal, and the blossom algorithm produces both. It is equivalent to the Tutte–Berge formula $\nu(G) = \min_{X} \tfrac12\bigl(|V| + |X| - \operatorname{odd}(G - X)\bigr)$ , it contains König's theorem as the case where all members of the cover are singletons, and it is the cardinality case of Edmonds' description of the matching polytope by odd-set constraints, which underlies weighted matching, $b$ -matching and the polyhedral approach to combinatorial optimization.

The theorem has been proved since 1965, with several independent proofs (via Tutte's theorem, via the Gallai–Edmonds decomposition, via linear programming). Mathlib contains Tutte's perfect-matching theorem for simple graphs, but neither the Tutte–Berge formula nor odd-set covers, alternating trees, blossom shrinking or Berge's augmenting-path theorem in a multigraph setting. This mission produces a machine-checked version of Edmonds' statement together with the lemmas of his algorithmic proof (4.12, 4.14, 4.15, 4.17), which are the correctness core of the blossom algorithm.

Difficulty

Weak duality and Berge's theorem are elementary. The difficulty is the strong direction. The obvious argument, a search for augmenting paths from an exposed vertex, fails because an alternating search tree in a non-bipartite graph can close an odd circuit, after which a vertex is reachable both by an even and by an odd alternating path; a naive search either misses augmenting paths or must back-track exponentially. The proof therefore has to work in shrunken graphs, whose vertices are nested sets of original vertices, and transfer maximality and covers back through every shrinking (4.12–4.15). Keeping track of nested blossoms, of the identity of edges under shrinking and of the parity bookkeeping of 5.8 is the main formal burden.

Formalization scope

Graphs are the published EdmondsMatching65.Polyhedron.Graph V E (a map from edges to unordered pairs of distinct vertices) with finite V, E; parallel edges are allowed and loops are not. Matchings are Finset E. Maximum and minimum are by cardinality, stated with explicit comparisons rather than sSup/sInf.
A family of odd sets is a Finset (Finset V); repeating a member only adds capacity, so this does not change the minimum. The capacity of a singleton is $1$ , not $(1-1)/2$ .
Paths and circuits are lists of vertices and edges; subgraphs are vertex and edge sets; a matching of a subgraph is a matching of $G$ using only its edges.
Shrinking is contraction along a partition of the vertices: the vertex type of $G/\mathcal P$ is the set of parts, the edge type is the set of edges not inside a part. Nested blossom shrinking is encoded by an inductive predicate of blossom sets (the complete expansions of pseudovertices), not by a tower of quotient types. Statements that shrink a set other than a circuit assume its induced subgraph connected, the standing assumption of 4.9.
5.7 is stated as the existence of a cover: the page's explicit families fail for the two-vertex graph with one edge and for the one-vertex graph, where the claim still holds.
5.8 is stated through the configuration the algorithm outputs (blossom sets, a planted Hungarian tree in $G'$ , pseudovertices outer), not through the algorithm as a procedure.
A trivializing formalization is excluded: the goal asserts the equality of the maximum and the minimum, not weak duality and not the separate existence of an optimal matching and an optimal cover.

Reusable beyond this mission: the multigraph shrinking construction, blossom sets, alternating and Hungarian trees, and Berge's theorem in the multigraph setting; these are shared with the companion mission on the invariance of the dual (Gallai–Edmonds). Proofs of any milestone, and alternative proofs of the goal (e.g. through Mathlib's Tutte theorem), are welcome.

Selected references

J. Edmonds, Paths, trees, and flowers, Canadian Journal of Mathematics 17 (1965), 449–467. https://doi.org/10.4153/CJM-1965-045-4
C. Berge, Two theorems in graph theory, Proceedings of the National Academy of Sciences USA 43 (1957), 842–844. https://doi.org/10.1073/pnas.43.9.842
W. T. Tutte, The factorization of linear graphs, Journal of the London Mathematical Society 22 (1947), 107–111. https://doi.org/10.1112/jlms/s1-22.2.107
J. Edmonds, Maximum matching and a polyhedron with 0,1-vertices, Journal of Research of the National Bureau of Standards 69B (1965), 125–130. https://doi.org/10.6028/jres.069B.013
L. Lovász and M. D. Plummer, Matching Theory, North-Holland, 1986. https://doi.org/10.1090/chel/367

16 thms3 active usersReviewed

Dynamic Programming Operations Research Optimization·Captain: mikedeng1

The Complexity of Markov Decision Processes III: The Optimal Discounted Cost of a Deterministic Process Is the Least Discounted Cost of a SigmaResearch Paper

Motivation

A Markov decision process with finitely many states and decisions, a discount factor $\beta\in(0,1)$ and the objective of minimizing expected discounted cost is the basic model of sequential decision making in operations research and reinforcement learning. It is solvable in polynomial time by linear programming. Papadimitriou and Tsitsiklis (Math. Oper. Res. 12(3), 1987) asked the finer question of whether it can be solved fast in parallel, and showed a sharp split: the general (stochastic) problem is P-complete (their Theorem 1), so it is unlikely to admit a polylogarithmic parallel algorithm, while the deterministic special case, where every transition probability is 0 or 1, is in NC (their Theorem 4).

The deterministic case is a shortest-path problem with a twist. Every policy traces a walk in a graph, and the cost of the walk counts its $t$ -th arc with weight $\beta^t$ . The paper's argument identifies the optimal discounted cost with the cost of a finite combinatorial object, a sigma, and computes it from discounted min-plus matrix products. This mission formalizes that identity.

Setting

A deterministic stationary Markov decision process consists of a finite set $S$ of $n$ states, an initial state $s_0\in S$ , and for each state $s$ a finite nonempty set $D_s$ of decisions. Decision $i\in D_s$ costs $c(s,i)\in\mathbb R$ and leads with certainty to the state $\mathrm{next}(s,i)$ . Equivalently, it is a directed graph on $S$ with an arc $s\to\mathrm{next}(s,i)$ of weight $c(s,i)$ for each decision; parallel arcs and loops are allowed.

A policy $\delta$ chooses a decision $\delta(s,t)\in D_s$ for every state $s$ and time $t=0,1,2,\dots$ ; it is stationary if $\delta(s,t)$ does not depend on $t$ . From $s_0$ it produces the states $s_{t+1}=\mathrm{next}(s_t,\delta(s_t,t))$ and the discounted cost

J_\beta(\delta)=\sum_{t=0}^{\infty}\beta^t c\bigl(s_t,\delta(s_t,t)\bigr).

The optimal discounted cost is $J^*_\beta(s_0)=\inf_\delta J_\beta(\delta)$ , the infimum over all policies $\delta(s,t)$ .

A sigma is a walk $w_0=s_0,w_1,\dots,w_N$ along decisions $e_t\in D_{w_t}$ whose nodes $w_0,\dots,w_{N-1}$ are distinct and whose last node repeats an earlier one, $w_N=w_j$ with $j<N$ : the walk from $s_0$ up to the first repetition of a node. It is a prefix of $j$ arcs followed by a cycle of $l=N-j\ge1$ arcs. Its discounted cost $c_\beta(P)$ is the discounted cost of the infinite walk that follows it and repeats its cycle forever.

In the min-plus semiring (addition is $\min$ , multiplication is $+$ , zero is $+\infty$ ), let $A_{uv}$ be the least cost of a decision from $u$ to $v$ ( $+\infty$ if none), let $rA$ multiply every finite entry by $r$ , and let

B_0=I,\qquad B_k=A\otimes\beta A\otimes\cdots\otimes\beta^{k-1}A ,

with $I$ the min-plus identity. The entry $(B_k)_{uv}$ is the least discounted cost $\sum_{t<k}\beta^t c_t$ of a $k$ -arc walk from $u$ to $v$ .

Formalization targets

Goal

For $0<\beta<1$ ,

J^*_\beta(s_0)=\min_{P\text{ sigma}}c_\beta(P)=\min\Bigl\{(B_k)_{s_0u}+\frac{\beta^{k}(B_l)_{uu}}{1-\beta^{l}}\;:\;u\in S,\ 0\le k\le n,\ 1\le l\le n,\ \text{both entries finite}\Bigr\},

with both minima attained. This is the claim on pp. 446–447 on which Theorem 4 rests. The algebraic expression is the corrected form of the paper's (see Formalization scope).

Milestones

The closed form of the cost of a sigma (p. 446): $c_\beta(P)=\sum_{t<j}\beta^tc_t+\frac{\beta^j}{1-\beta^l}\sum_{t<l}\beta^tc_{j+t}$ .
A stationary optimal policy exists (§2, p. 444; cited on p. 446). The general finite stochastic statement is on the platform as BertsekasDP.discounted_main_theorem (Proved), and the deterministic case is stated in this mission's model.
The path of a stationary policy, cut at its first repeated node, is a sigma with the same discounted cost, and every sigma arises this way (p. 446).
The products $B_j$ are the cheapest discounted $j$ -arc walks (p. 447).

Significance

The identity reduces an optimization over infinite objects, the time-dependent policies, to a minimum over finitely many closed-form expressions in matrix entries. Each $B_k$ is a product of $k$ min-plus matrices, and matrix products parallelize well; that is the source of the NC algorithm. The same reduction, with the discounting removed, underlies the minimum-mean-cycle characterization of the average-cost problem (mission II of this series), and the sigma structure reappears in the stationary finite-horizon analysis (mission IV).

On the formalization side, the result has been proved in the paper only as a short paragraph, which cites the existence of stationary optimal policies and leaves the algebra to the reader. Its printed formulas contain index slips (below). A machine-checked version fixes the exact constants. To our knowledge none of these statements has a formal proof. The existence of stationary optimal policies for finite discounted problems is formalized on the platform in Bertsekas's general stochastic setting.

Difficulty

The obvious argument says: an optimal policy may be taken stationary, a stationary deterministic policy produces an eventually periodic path, and an eventually periodic path is a sigma. The first step is the substantial one: the optimum is an infimum over all time-dependent policies $\delta(s,t)$ , and a non-stationary policy can follow any walk at all, so this step is a statement about the whole dynamic program, not a combinatorial fact about a single walk. The second part of the goal adds a matching argument in the other direction: the expression ranges over arbitrary $k$ -arc walks and closed $l$ -walks, which need not be simple, so one must check that none of them beats the best sigma, and that the best sigma has $k\le n$ and $l\le n$ . Finally, the discount factors must be tracked exactly; the printed formulas are off by one power of $\beta$ in two places.

Formalization scope

The Lean development lives in the namespace MDPComplexity.Discounted, with one definition file and five theorems. Conventions committed to:

The model is stationary and deterministic. A DetMDP S has a finite state type, a nonempty finite decision type at each state (the paper says "a finite set $D_s$ "; nonemptiness is implicit since a policy must choose a decision), a successor map and real costs.
Policies are maps $\delta(s,t)$ , time is $\mathbb N$ from $0$ , and the optimum optDisc is the infimum over all such policies. Defining it over stationary policies or over sigmas would make the goal true by definition. That shortcut is ruled out, and the stationarity step is part of the content.
Costs are tsums, which are junk ( $0$ ) for non-summable series; every statement that sums costs assumes $0<\beta<1$ , under which the series converge absolutely.
A sigma is encoded as a lasso, $w_N=w_j$ with $j<N$ . This includes $j=0$ , a sigma whose cycle passes through $s_0$ , which the printed form $(u_0,\dots,u_k,v_1,\dots,v_l,v_1)$ omits but the definition "a path from $u_0$ until the first repetition of a node" includes. The paper's $k$ is $j-1$ .
Corrected slips: (i) in the sigma display the cycle sum carries $\beta^{j-1}$ , not $\beta^j$ , for its $j$ -th arc, and the indices are made consistent; (ii) the algorithm's expression is $\lambda+\beta^k\mu/(1-\beta^l)$ with $l\ge1$ , not $\lambda+\beta^{k+1}\mu/(1+\beta^l)$ (one state with a loop of cost $1$ has optimum $1/(1-\beta)$ , which the printed form misses); (iii) $B_0$ , used but not defined, is the min-plus identity.
Matrix entries are in Tropical (WithTop ℝ), so $+\infty$ is ⊤ and the product is Mathlib's matrix product over the tropical semiring.

Not formalized: membership in NC, the processor count $n^4$ , the $\log^2 n+3\log n$ parallel time, and the P-completeness of the general problem. Mathlib has no parallel complexity classes. Only the identity that makes the algorithm correct is a target.

Contributions welcome: proofs of any milestone. A bridge from DetMDP to BertsekasSSPModel (taking decisions as controls and 0/1 transition rows) would let milestone 2 be derived from the platform's proved Proposition 7.3.1. A direct proof of the deterministic case is also welcome. The lasso and walk lemmas are reusable for the other missions of the series.

Selected references

C. H. Papadimitriou and J. N. Tsitsiklis, The Complexity of Markov Decision Processes, Mathematics of Operations Research 12(3), 441–450, 1987. https://doi.org/10.1287/moor.12.3.441
D. P. Bertsekas, Dynamic Programming and Optimal Control, Vol. I, 3rd ed., Athena Scientific, 2005, §7.3 (discounted problems, Proposition 7.3.1).
M. L. Puterman, Markov Decision Processes: Discrete Stochastic Dynamic Programming, Wiley, 1994, Ch. 6 (existence of stationary optimal policies for discounted models). https://doi.org/10.1002/9780470316887

7 thms3 active usersReviewed

Complexity Theory Operations Research Theoretical Computer Science·Captain: mikedeng1

Complexity of Machine Scheduling Problems 6: DIRECTED HAMILTON PATH Reduces to No-Wait Flow Shop Makespan and Total Completion TimeResearch Paper

Motivation

In a no-wait flow shop every job passes through the machines $M_1,\dots,M_m$ in the same order, and once it has started it may never wait between two machines. The constraint comes from processes in which the material changes state if it is left standing, such as hot metal rolling, chemical and food processing, and some pharmaceutical lines; see the survey of Hall and Sriskandarajah (doi:10.1287/opre.44.3.510). The question of how hard it is to schedule such a shop well is the question this mission formalizes.

Brucker, Lenstra and Rinnooy Kan settled it for the case in which the number of machines is part of the input. In their report Complexity of Machine Scheduling Problems (Mathematisch Centrum, 1975; journal version in Annals of Discrete Mathematics 1, 1977, doi:10.1016/S0167-5060(08)70743-X), Theorem 5 reduces DIRECTED HAMILTON PATH to the no-wait flow shop. Both minimizing the makespan $C_{\max}$ and minimizing the total completion time $\sum C_j$ are thereby NP-complete.

Timeline.

1964: Gilmore and Gomory solve the two-machine no-wait flow shop with makespan in polynomial time (doi:10.1287/opre.12.5.655).
1972: Wismer (doi:10.1287/opre.20.3.689) and Reddi and Ramamoorthy (doi:10.1057/jors.1972.52) show that no-wait makespan minimization is a travelling-salesman problem with arc weights computed from the processing times.
1972: Karp proves DIRECTED HAMILTON CIRCUIT NP-complete (doi:10.1007/978-1-4684-2001-2_9).
1975: Brucker, Lenstra and Rinnooy Kan reduce DIRECTED HAMILTON CIRCUIT to DIRECTED HAMILTON PATH (their Theorem 2(d)), and DIRECTED HAMILTON PATH to $n|m|F,\textit{no wait}|C_{\max}$ and to $n|m|F,\textit{no wait},w_j=1|\sum w_jC_j$ (Theorem 5).
1984: Röck shows that the problem stays NP-hard for three machines (doi:10.1145/62.65).

Setting

There are $n$ jobs $J_1,\dots,J_n$ and $m$ machines. Job $J_\ell$ needs processing time $p_{\ell i}\in\mathbb N$ on machine $M_i$ . Write

q_{\ell i}=\sum_{r=1}^{i}p_{\ell r},\qquad q_{\ell 0}=0,

for the time job $J_\ell$ spends on its first $i$ machines. Because a job never waits, a schedule is determined by the start times $B_\ell\in\mathbb N$ . The operation of $J_\ell$ on $M_i$ occupies $[B_\ell+q_{\ell,i-1},\,B_\ell+q_{\ell i})$ , and job $J_\ell$ completes at $C_\ell=B_\ell+q_{\ell m}$ . A schedule is feasible when no two distinct jobs occupy the same machine at the same time. The delay

c_{jk}=\max_{1\le i\le m}\{q_{ji}-q_{k,i-1}\}

is the least gap $B_k-B_j$ that lets $J_k$ follow $J_j$ on every machine.

A directed graph $G=(V,A)$ on $V=\{0,\dots,n-1\}$ has a Hamilton path if its vertices can be ordered $\sigma(0),\dots,\sigma(n-1)$ with every $(\sigma(i),\sigma(i+1))\in A$ .

From $G$ the paper builds an instance with $n$ jobs and $m=n(n-1)+2$ machines. Each ordered pair $(j,k)$ of distinct jobs is assigned a middle machine $\iota(j,k)\in\{2,\dots,m-1\}$ , and the partial sums $q_{\ell i}$ are perturbed from $i\mu$ by $\pm\lambda$ or $\pm(\lambda+1)$ on the machines $\iota(\ell,\cdot)$ and just before the machines $\iota(\cdot,\ell)$ , depending on whether the pair is an arc. The parameters satisfy $\lambda\ge1$ and $\mu\ge2\lambda+3$ .

Formalization targets

Goal (Theorem 5)

\text{DIRECTED HAMILTON PATH}\ \propto\ n|m|F,\textit{no wait}|C_{\max}\quad\text{and}\quad \text{DIRECTED HAMILTON PATH}\ \propto\ n|m|F,\textit{no wait},w_j=1|\textstyle\sum w_jC_j,

where $\propto$ is polynomial-time many-one reducibility between the binary-coded recognition languages.

Milestones, in the order the proof uses them

Eq. (9): $c_{jk}$ is the least gap between $B_j$ and $B_k$ for which $J_k$ follows $J_j$ on every machine.
The travelling-salesman reformulation: if all processing times are positive, a feasible schedule with $C_{\max}\le y$ (resp. $\sum C_\ell\le y$ ) exists iff some job order has path length (resp. summed completion times along the path) at most $y$ .
An admissible ordering $\iota$ exists for every $n\ne2$ .
All processing times of the construction are at least $1$ .
The delays of the construction: $c_{jk}=\mu+2\lambda$ if $(j,k)\in A$ , and $\mu+2\lambda+2$ otherwise.
Theorem 5(a), the equivalence: $G$ has a Hamilton path $\iff$ $C_{\max}\le(n-1)(\mu+2\lambda)+m\mu$ .
Theorem 5(b), the equivalence: $G$ has a Hamilton path $\iff$ $\sum_jC_j\le\tfrac12n(n-1)(\mu+2\lambda)+nm\mu$ .
Theorem 2(d), off the goal's path: $G'$ has a Hamilton circuit iff the graph obtained by splitting a vertex $v'$ into $v'$ and a new sink $v''$ has a Hamilton path.

Significance

The result. Theorem 5, together with the NP-completeness of DIRECTED HAMILTON PATH, places both no-wait criteria among the NP-complete problems once $m$ is part of the input. The Gilmore–Gomory algorithm for two machines therefore cannot be extended to arbitrary $m$ unless P = NP, and heuristics and exact exponential methods for no-wait shops are justified. The reduction also gives a structural fact of independent use: every directed graph can be realized, up to two arc-weight values, as the delay matrix of a no-wait flow shop.

Formalizing it. The result has been proved for fifty years; to our knowledge no machine-checked version exists. This mission produces a checked no-wait flow shop model, a checked travelling-salesman reformulation of it, the correctness of the paper's construction, and a polynomial-time reduction in an explicit Turing-machine model. It also records a gap in the printed proof: the ordering $\iota$ the paper calls easy to construct does not exist for $n=2$ .

Difficulty

Three steps are not routine.

The passage from schedules to job orders assumes that the order in which jobs start is the order in which they visit every machine. With zero processing times this fails, so the reformulation needs the positivity milestone.
Computing the delays requires a case analysis over all machines and all pairs of perturbations. The property of $\iota$ is exactly what keeps the " $+$ " and " $-$ " cases from colliding, and the constants $\lambda\ge1$ , $\mu\ge2\lambda+3$ are tight enough that the comparison must be done carefully.
The goal asks for an actual Turing machine with a polynomial step bound. It has to build $\iota$ for every $n\ne2$ and handle $n\le2$ separately. The equivalences alone do not give this.

Formalization scope

Jobs and machines are $0$ -based (Fin n, Fin m); cum p ℓ i is the paper's $q_{\ell i}$ , and the machine indices $\iota(j,k)$ are the paper's $1$ -based indices. Start times are natural numbers, and release dates are $0$ . Section 3 computes times from processing orders on integer data, and every criterion is regular, so real start times would not change the yes-instances. A zero-length operation occupies the empty interval. $C_{\max}\le y$ is stated as $C_\ell\le y$ for every job. The delays, the partial sums of the construction and its processing times are computed in $\mathbb Z$ . The instance uses their conversion to $\mathbb N$ , which is exact by milestone 4. The threshold of Theorem 5(b) is compared in $\mathbb Q$ , as printed.

The paper's loose phrases are made explicit as follows:

"scheduled directly after" means "precedes on every machine";
"equivalent to solving the TRAVELLING SALESMAN problem" means the two threshold equivalences of milestone 2, with the $\sum C_j$ version as the reading of "constructed as in (a)";
"such an ordering can easily be constructed" is stated for $n\ne2$ , the only case in which it is true.

Directed graphs are Boolean adjacency matrices. A graph with $0$ or $1$ vertices has a Hamilton path, and a one-vertex graph has a Hamilton circuit iff it has a loop.

The goal is CookPvsNP.PolyReducible from the published definition CookPvsNP_defs, with polynomial time measured on Cook's one-tape Turing machines. Instances are coded with the alphabet BSym and binary code encNats of the published ProjSchedTW.Complexity.Encoding (Neumann, Schwindt and Zimmermann). A graph is coded as $n$ followed by its adjacency matrix; a flow-shop instance as $n$ , $m$ , the matrix $(p_{\ell i})$ and the threshold $y$ .

Stating only the equivalences 6–7 and calling the result "reducible" would drop polynomiality; the goal therefore asserts PolyReducible. The target languages contain exactly the no-wait flow-shop instances, with no waiting allowed, so the reduction cannot land in a looser problem. The parameters $\lambda,\mu$ always carry $\lambda\ge1$ , $\mu\ge2\lambda+3$ .

Contributions are welcome at every level:

the general travelling-salesman reformulation, which is reusable for any no-wait flow-shop result;
the combinatorial existence of $\iota$ ;
the arithmetic of the construction;
Turing-machine infrastructure for computing arithmetic list transformations in polynomial time, which every reduction in this series needs.

Selected references

P. Brucker, J. K. Lenstra, A. H. G. Rinnooy Kan, Complexity of Machine Scheduling Problems, Mathematisch Centrum Report BW 43/75, Amsterdam, 1975; Annals of Discrete Mathematics 1 (1977) 343–362. doi:10.1016/S0167-5060(08)70743-X
R. M. Karp, Reducibility among combinatorial problems, in Complexity of Computer Computations, Plenum, 1972, 85–103. doi:10.1007/978-1-4684-2001-2_9
P. C. Gilmore, R. E. Gomory, Sequencing a one state-variable machine: a solvable case of the traveling salesman problem, Operations Research 12 (1964) 655–679. doi:10.1287/opre.12.5.655
D. A. Wismer, Solution of the flowshop-scheduling problem with no intermediate queues, Operations Research 20 (1972) 689–697. doi:10.1287/opre.20.3.689
S. S. Reddi, C. V. Ramamoorthy, On the flow-shop sequencing problem with no wait in process, Operational Research Quarterly 23 (1972) 323–331. doi:10.1057/jors.1972.52
H. Röck, The three-machine no-wait flow shop is NP-complete, Journal of the ACM 31 (1984) 336–345. doi:10.1145/62.65
N. G. Hall, C. Sriskandarajah, A survey of machine scheduling problems with blocking and no-wait in process, Operations Research 44 (1996) 510–525. doi:10.1287/opre.44.3.510
S. A. Cook, The complexity of theorem-proving procedures, STOC 1971, 151–158. doi:10.1145/800157.805047

14 thms3 active usersReviewed

Dynamic Programming Operations Research Optimization·Captain: mikedeng1

Send-and-Split Method for Minimum-Concave-Cost Network Flows II: Subproblem Minimum Costs Are the Greatest Solution of the Send-and-Split Equations, Unique if Circulations Cost Positively (Theorem 2)Research Paper

Motivation

Many network-design and production-planning problems ask for a cheapest way to route a commodity from supply points to demand points when the cost of an arc grows less than proportionally with the amount sent: setup charges, economies of scale, and fixed-plus-linear costs all give concave arc costs. Minimizing a concave function over the flow polytope is NP-hard in general, and the classical linear-cost machinery (potentials, negative-cycle tests) no longer applies. Erickson, Monma and Veinott (Math. Oper. Res. 12 (1987)) gave the send-and-split method, a dynamic program over subsets of the demand nodes that solves the uncapacitated problem in time polynomial in the number of nodes and arcs and exponential only in the number of demand nodes. It contains as special cases the Dreyfus–Wagner recursion for Steiner trees in graphs (Networks 1 (1971)), and the paper applies it to concave-cost production, inventory and network-design problems (§6).

Timeline. Zangwill (1968) solved minimum-concave-cost flows on special networks by dynamic programming. Dreyfus and Wagner (1971) gave the subset recursion for Steiner trees with positive arc lengths. Erickson, Monma and Veinott (1987) extended the subset recursion to arbitrary uncapacitated networks with additive concave arc costs and arbitrary real demands, proved that the minimum costs of the subproblems form the greatest solution of the resulting equations (Theorem 2), and showed it is the only solution when every simple circulation has positive cost.

Setting

A network consists of a directed graph $G = (N, A)$ with nodes $N = \{0, \dots, n-1\}$ and arcs $A$ , ordered pairs of distinct nodes, together with a real demand vector $r = (r_i)$ . A preflow is a nonnegative matrix $x = (x_{ij})$ supported on $A$ ; a flow for $r$ is a preflow with inflow minus outflow equal to $r_i$ at every node. Each arc has a cost function $c_{ij}$ , concave on $[0, \infty)$ with $c_{ij}(0) = 0$ , and the cost of a preflow is $c(x) = \sum_{(i,j)\in A} c_{ij}(x_{ij})$ . A minimum-cost flow is a flow whose cost is at most that of every flow. A simple circulation is a circulation equal to some $\theta > 0$ on the arcs of a simple directed circuit and $0$ elsewhere.

The demand nodes are $D = \{ i : r_i \neq 0 \}$ . For $\emptyset \subset I \subseteq D$ let $r_I = \sum_{j \in I} r_j$ . The subproblem $i \to I$ keeps the demands of the nodes in $I$ , sets all others to zero, and subtracts $r_I$ at node $i$ ; $C_{iI}$ is its minimum cost, $+\infty$ when it has no flow. Let $A_I = A$ if $r_I > 0$ and the reversed arcs if $r_I < 0$ , with sending cost $c_{ij}(r_I)$ , read as $c_{ji}(-r_I)$ when $r_I < 0$ . The send-and-split equations for an array $C'$ are

C'_{iI} = C'_{j, I\setminus\{j\}} \ (j \in I) \quad \text{if } r_I = 0, \qquad (1)

C'_{iI} = \min_{(i,j)\in A_I} \bigl[ c_{ij}(r_I) + C'_{jI} \bigr] \wedge B'_{iI} \quad \text{if } r_I \neq 0, \qquad (2)

with $B'_{iI} = \min_{\emptyset\subset J\subset I} [C'_{iJ} + C'_{i,I\setminus J}]$ for $|I| > 1$ , and $B'_{iI} = 0$ if $I = \{i\}$ , $+\infty$ otherwise, for $|I| = 1$ (3).

Formalization targets

Goal: Theorem 2 (Dynamic-Programming Equations)

If there is a minimum-cost flow for $r$ , then

C \text{ solves (1)–(3)}, \qquad C'_{jI} \le C_{jI} \ \text{ for every } +\infty\text{-or-real solution } C',

for all $j \in N$ and $\emptyset \subset I \subseteq D$ . If moreover every simple circulation has positive cost, then every $+\infty$ -or-real solution equals $C$ .

Milestones

In attack order: the subproblem alternative (a minimum-cost flow or no flow, p. 640); equation (1); inequalities (4), (5), (6) (p. 641); $C_{iI} = B_{iI}$ for $i \in I$ (p. 641); $C$ satisfies (1) and (2) (p. 642); and two generic statements about Bellman's equations (2)′ for minimum-cost chains in a graph with nonnegative, respectively positive, simple circuits: the minimum chain costs form the greatest solution and are nondecreasing in the arc costs, and with positive circuits the solution is unique (p. 642).

Significance

Theorem 2 is the correctness theorem of the send-and-split method: it says that solving equations (1)–(3) by increasing $|I|$ , with a shortest-chain computation for each $I$ , yields the true subproblem minimum costs, in particular the optimum $C_{iD}$ of the original problem. Its uniqueness clause identifies when the equations alone determine the answer, and the counterexample on p. 641 (zero costs on a strongly connected graph) shows that the positivity hypothesis cannot simply be dropped. The same structure underlies the Steiner-tree recursion.

The theorem is proved in the paper; to our knowledge none of it is formalized. This mission supplies Lean definitions of uncapacitated concave-cost flows with extended-real minimum costs and the send-and-split equations, and poses the correctness theorem as a proof goal. The two Bellman milestones are general facts about minimum-cost chains with $+\infty$ -or-real values and are reusable well beyond this paper. Related items on the platform are credited, not reused: the Dreyfus–Wagner Steiner recursion DreyfusWagner.Steiner.steinerLength_recurrence and DreyfusWagner.Steiner.optimal_decomposition (the special case of undirected positive lengths), and BellmanRouting.PolicySpace.routing_equation_unique (uniqueness of the routing equation on a complete graph with positive real times).

Difficulty

The equations (2) mix two minima: sending the whole demand $r_I$ across one arc, and splitting $I$ at the current node. Showing that $C$ satisfies them requires that some optimal flow of every subproblem has a tree-like structure, which in turn rests on the existence theory for concave-cost flows (an optimum is attained at an extreme flow whose support is a forest). Showing that $C$ is the greatest solution requires an induction on $|I|$ in which, for fixed $I$ , equation (2) is a shortest-chain system whose arc costs to an auxiliary node depend on the solution at smaller sets; comparison then needs monotonicity of minimum chain costs in the arc costs, including arcs whose cost drops from $+\infty$ . The naive attempt to prove uniqueness by iterating (2) fails without the positivity hypothesis, because zero-cost circuits admit spurious solutions.

Formalization scope

Nodes are Fin n; arcs are a Finset (Fin n × Fin n) with no loops; arc costs are functions $\mathbb{R} \to \mathbb{R}$ assumed concave on Set.Ici 0 with $c_{ij}(0) = 0$ at arcs (the paper's standing assumption, stated as a hypothesis). Minimum costs, sending costs, splitting terms and solutions take values in EReal; the empty infimum is $+\infty$ , as on the page.

Explicit readings of the paper's phrases:

"there is a minimum-cost flow" means a flow for $r$ whose cost is at most that of every flow for $r$ ;
" $+\infty$ or real-valued" means $\neq -\infty$ , required on every $\emptyset \subset I \subseteq D$ ;
"greatest solution" is two claims: $C$ is a solution, and every solution is $\le C$ entrywise;
"each simple circulation has positive cost" quantifies over every simple circuit and every $\theta > 0$ ;
" $C_{iI}$ is finite" is rendered as $C_{iI} = c(x)$ for a minimum-cost flow $x$ of the subproblem;
"minimum-cost chain" is the infimum of walk costs, attained or $+\infty$ ; arc costs of $+\infty$ in (2)′ are missing arcs.

The definition of $C_{iI}$ is the infimum over flows, never the equations themselves; a formalization defining $C$ by (1)–(3), or omitting the $\neq -\infty$ condition on solutions, or dropping the clause that $C$ is itself a solution, would make the theorem trivial or false and is ruled out. Arrays are compared only on admissible sets. The graph structure of (2)′ is the platform definition BertsekasSPGraph. Running-time bounds, the planar refinements of §4 (Theorem 3) and the capacitated reduction of §5 are out of scope. Proofs of any milestone, and a formalization of the paper's Theorem 1 that the proofs rely on, are welcome.

Selected references

R. E. Erickson, C. L. Monma, A. F. Veinott, Jr., Send-and-Split Method for Minimum-Concave-Cost Network Flows, Mathematics of Operations Research 12(4), 1987, 634–664. https://doi.org/10.1287/moor.12.4.634
S. E. Dreyfus, R. A. Wagner, The Steiner Problem in Graphs, Networks 1(3), 1971, 195–207. https://doi.org/10.1002/net.3230010302
R. Bellman, On a Routing Problem, Quarterly of Applied Mathematics 16(1), 1958, 87–90. https://doi.org/10.1090/qam/102435
W. M. Hirsch, A. J. Hoffman, Extreme Varieties, Concave Functions, and the Fixed Charge Problem, Communications on Pure and Applied Mathematics 14(3), 1961, 355–369. https://doi.org/10.1002/cpa.3160140312
W. I. Zangwill, Minimum Concave Cost Flows in Certain Networks, Management Science 14(7), 1968, 429–450. https://doi.org/10.1287/mnsc.14.7.429

15 thms3 active usersReviewed

Completed

Linear Optimization Operations Research Optimization·Captain: mikedeng1

Finding Minimum-Cost Circulations by Successive Approximation II: For Real Costs, the Strongly Polynomial Loop Reaches a Minimum-Cost Circulation After at Most m⌈log₂(2n)⌉ RefinementsResearch Paper

Why minimum-cost circulation needs a real-cost iteration bound

A minimum-cost circulation is a way to send flow around a directed network while respecting capacities and paying a cost per unit on each arc. It is a basic form of network optimization: a minimum-cost flow with prescribed supplies and demands can be reduced to a circulation problem, and the circulation formulation exposes the residual arcs on which a flow can be improved. Goldberg and Tarjan's successive-approximation method relaxes exact optimality by an error parameter and repeatedly reduces that error. Its ordinary stopping rule for integer costs depends on the largest cost. For arbitrary real costs, including irrational costs, a decreasing positive error need never cross a fixed numerical cutoff. The strongly polynomial loop in their 1987 technical report, later published in Mathematics of Operations Research instead tests the smallest error parameter appropriate to the current circulation and stops when it is zero.

This mission formalizes the number of refinement calls made by that loop. It builds on the related Goldberg–Tarjan 1988 max-flow and 1989 minimum-mean cycle-canceling series: those develop different algorithms for network flow, while the published 1989 circulation and approximate-optimality definitions provide this mission's common network model. The result here concerns successive approximation and its fixed-arc progress measure.

Network and approximate optimality

The vertex set $V$ is finite, with $n=|V|$ , and $E$ is a symmetric set of directed arcs, with $m=|E|$ . Symmetry means that $(v,w)\in E$ brings $(w,v)\in E$ too. Each arc has a real capacity $u(v,w)$ and a real cost $c(v,w)$ ; costs obey $c(v,w)=-c(w,v)$ . A circulation $f$ obeys $f(v,w)\le u(v,w)$ , $f(v,w)=-f(w,v)$ , and conservation of flow at every vertex. Its total cost is half the sum of $c(v,w)f(v,w)$ over directed arcs, since each unordered edge appears twice. A minimum-cost circulation costs no more than any other circulation of the network.

The residual capacity is $u_f(v,w)=u(v,w)-f(v,w)$ . For a price function $p:V\to\mathbb R$ , the report writes the reduced cost as $c_p(v,w)=c(v,w)-p(v)+p(w)$ . A circulation is $\varepsilon$ -optimal with respect to $p$ when every residual arc has reduced cost at least $-\varepsilon$ . It is $\varepsilon$ -optimal if some price function works, where $\varepsilon\ge0$ . The tight error $\varepsilon(f)$ is the least such error. A circulation is $\varepsilon$ -tight when it is $\varepsilon$ -optimal but fails to be $\varepsilon'$ -optimal at every $\varepsilon'<\varepsilon$ . This includes attainment at $\varepsilon$ .

An arc is $\varepsilon$ -fixed if all $\varepsilon$ -optimal circulations carry the same flow through it. Write $F_\varepsilon$ for the set of these arcs. Theorem 4.2 supplies an arc-fixing criterion from a large absolute reduced cost. Lemma 4.4 says that when a positive tight error falls by a factor of $2n$ , $F_\varepsilon$ becomes strictly larger. Both are numbered results on printed pages 16–17 of the source report's journal counterpart.

Formalization targets

The goal is the circulation-level form of Theorem 4.5. Begin with a circulation $f_0$ and a sequence $f_0,f_1,\ldots$ whose positive-error steps satisfy the contract of Figure 3: if $\varepsilon(f_k)>0$ , the next circulation is $\varepsilon(f_k)/2$ -optimal. With the report's standing $n\ge2$ and $m\ge n-1$ , the target is

\exists k\le m\left\lceil\log_2(2n)\right\rceil:\quad \varepsilon(f_k)=0\quad\text{and}\quad f_k\text{ is minimum-cost}.

The milestone list contains the already proved complementary-slackness characterization of minimum cost (Theorem 2.2), the cross-parameter arc-fixing result (Theorem 4.2), and strict growth of fixed arcs (Lemma 4.4). The report states Theorem 4.5 as $O(m\log n)$ iterations when each refinement decreases error by a constant factor. The target makes explicit the factor two used by the paper's refinements and the resulting finite count.

What the result establishes

The theorem gives a bound on the number of refinement calls that depends on the number of vertices and arcs, not on the magnitude, precision, or integrality of the costs. It gives an exact minimum-cost circulation rather than an arbitrary small-error approximation. This distinguishes the real-cost loop from an integer-cost stopping rule based on $1/n$ . The bound counts refinement calls only; the report analyzes the work within particular implementations separately.

The published 1989 definitions and the complementary-slackness theorem already have machine-checked status on the platform. Theorem 4.2, Lemma 4.4, and this iteration theorem are the open formalization targets. A complete development will connect the tight error to residual-cycle structure, establish that its infimum is attained for circulations, and prove that zero tight error implies minimum cost. The mission thereby makes the fixed-arc argument reusable for other circulation algorithms that lower an approximate-optimality parameter.

Why the bound needs more than repeated halving

Repeatedly dividing a positive real error by two gives errors approaching zero, but it does not by itself produce a finite step with zero error. The missing finite progress is structural: an arc must become fixed after enough reductions, and only finitely many arcs exist. Proving that fixedness is strict is delicate because it compares all circulations at two different error levels, not just two consecutive flows. Theorem 4.2 is the quantitative bridge between a price certificate for one flow and agreement of an arc across every sufficiently accurate flow. At the boundary $\varepsilon=0$ , the printed wording of Lemma 4.4 would require $F_0$ to be a proper subset of itself, so its positive-error regime must be made explicit.

Formalization scope

The Lean network uses CycleCanceling.MinMean.CircNetwork with a finite vertex type, a finite symmetric arc set, and real-valued capacities, costs, and flows. Off-arc values of these functions are irrelevant. The report assumes $m\ge n-1\ge1$ on printed page 5; the theorem binders express it as $n\ge2$ and $m\ge n-1$ . The arc count is for ordered arcs, exactly as the report defines $m$ . No integrality, rounding, or bounded-cost hypothesis is imposed. A feasible initial circulation is required because Figure 3 starts from one; infeasibility detection is outside this target.

The reused 1989 definitions write reduced cost as $c(v,w)+p(v)-p(w)$ . Substituting $-p$ for $p$ gives the report's $c(v,w)-p(v)+p(w)$ , so existential price certificates, $\varepsilon$ -optimality, and absolute reduced-cost conditions agree. The tight error is represented by a real infimum; proving that it is attained is part of the work. The set $F_\varepsilon$ is filtered from $E$ and includes only arcs whose flow is shared by all $\varepsilon$ -optimal circulations. The halving run computes its error from the current circulation; it does not take an unrelated error sequence. Once that error is zero, the loop has returned and later sequence entries are unconstrained. These choices exclude a vacuous or artificially fixed error parameter and a preselected optimal flow.

The explicit reading of the report's asymptotic count is $t=\lceil\log_2(2n)\rceil$ halvings per factor- $2n$ reduction and at most $m$ such blocks, giving $m t$ refinements. This is a statement about refinement count, not a RAM-operation bound. Contributions on Theorem 4.2, the residual-cycle characterization of positive tight error, the fixed-arc strictness lemma, and the final finite counting argument all support the goal. The circulation, price, and fixed-arc infrastructure can be reused beyond this particular implementation.

Selected references

A. V. Goldberg and R. E. Tarjan, Finding Minimum-Cost Circulations by Successive Approximation, MIT/LCS/TM-333, July 1987; journal version in Mathematics of Operations Research 15(3), 1990, pp. 430–466. DOI: 10.1287/moor.15.3.430. The mission's page and theorem indices refer to the 1987 report.

9 thms3 active usersReviewed

Missions

Dynamic Programming and Optimal Control II: Label Correcting MethodsTextbook

Motivation

Setting

Target

Significance

Difficulty

Formalization scope

Selected references

Sands–Sauer–Woodrow: monochromatic paths in two-coloured tournamentsResearch Paper

Motivation

Setting

Formalization targets

Goal — the two-coloured tournament theorem (SSW Corollary 2)

Milestone — the two-coloured digraph theorem (SSW Theorem 1)

Milestone — the source form of the goal

Milestone — the blocked three-coloured theorem (SSW Theorem 3)

Significance

Difficulty

Formalization scope

Selected references

Quantum Expander Codes: On a Biregular Left-Right Expanding Graph with δA, δB < 1/6, the Greedy Generator Decoder Corrects Every Quantum Error of Weight Below min(γA·nA, γB·nB)/(3(1+ΔB))Research Paper

Motivation

Setting

Formalization targets

Goal: Theorem 2

Milestones

Significance

Difficulty

Formalization scope

Selected references

A Solution to the 1-2-3 Conjecture: Every Finite Graph Without a K2 Component Has an Edge-Weighting from {1,2,3} Whose Weighted Degrees Properly Color the VerticesResearch Paper

Motivation

Setting

Formalization targets

Goal: Theorem 1 (p. 2)

The connected case (p. 14)

Milestones along the proof

Significance

Difficulty

Formalization scope

Selected references

Generalized Turán Problems for Even Cycles 6: The Maximum Number of (2l+1)-Cycles in a Graph with No Cycle of Length 3, …, 2l or 2k+1 Is Ω(n^{1+1/(2k+2)}) and O(n²)Research Paper

Motivation

Setting

Formalization targets

Goal: Theorem 18

Milestones

Significance

Difficulty

Formalization scope

Selected references

Twin-width I: Tractable FO Model Checking 1: Every Graph with Boolean-width k Has Twin-width at Most 2^(k+1) − 1Research Paper

Motivation

Setting

Formalization targets

Goal: Theorem 4.2 (p. 3:14)

Milestones (proof of Theorem 4.2, p. 3:14)

Significance

Difficulty

Formalization scope

Selected references

A proof of Seymour’s second-neighborhood conjectureOpen Problem

Motivation

Setting

Formalization target

Significance and status

Difficulty

Formalization scope

Selected references

A Sharp Threshold Bound for Monotone Graph PropertiesResearch Paper

Motivation: how sharp is the threshold of a graph property?

Timeline

Setting

Formalization targets

Goal: the Friedgut–Kalai sharp-threshold conjecture (Theorem 1.1)

Significance

Difficulty

Formalization scope

Goal: $\psi'$ solves the bottleneck traveling salesman problem