Graph Theory

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)

1. 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)}$.
2. 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))\}$.
3. For every $\varphi$: $E(\varphi^2)\le\frac{\iota}{2}\big(E(\varphi^2)+\langle\varphi,P\varphi\rangle_{L^2(\pi)}\big)$.
4. 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

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

1. Every consistent set is a union of equivalence classes (§6, p. 25): $\kappa \in \mathcal C \Rightarrow [\kappa] \subseteq \mathcal C$.
2. 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}$.
3. Claim (2): if $\mathcal A_{13} \subseteq \mathcal C$ then $\mathcal C$ includes one of $\mathcal A_{23}, \mathcal A_{35}$.
4. 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

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

1. 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.
2. LP duality (§2.2, p. 796): every distance function satisfying (5) has $W\ge f$, and some such function has $W=f$.
3. 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.
4. 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$.
5. 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$.
6. 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.

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

1. 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$.
2. 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.
3. 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)}$.
4. $\varphi$ minimizes $m$ (p. 671): $m(\varphi)\le m(\psi)$ for every permutation $\psi$.
5. 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$.
6. 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

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

1. Finite-capacity cutsets of $G^*$ correspond to initial sets $I=T-\{t\}$ (p. 14).
2. A finite cutset has capacity $\sum_{j\in N}\max(0,w_j)-\sum_{j\in I}w_j$ (p. 15).
3. A minimum cutset yields a maximum-weight initial set (p. 15).
4. 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).
5. Every attainable ratio lies in $[-w^*,w^*]$ (p. 16).
6. 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

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:

1. if $\mathrm{cl}(A\cup\{(j,b)\})$ is independent, the procedure moves there;
2. otherwise, if $\mathrm{cl}(A\cup\{(j,\lnot b)\})$ is independent, it moves there;
3. 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

1. A teacher available in at most $2$ periods has at most $2$ possible schedules.
2. CT4 has a solution iff its conflict graph has $n$ pairwise non-adjacent nodes.
3. The implications of chosen nodes lie inside every timetable that contains those nodes.
4. If $A$ is independent and closed under implications, $G$ has a timetable iff it has one containing $A$.
5. 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

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:

1. Theorem 1: $c(\varphi)=\min_\psi c(\psi)$ over all permutations.
2. 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)$.
3. Lemma 1: an interchange between two different cycles merges them.
4. Theorem 2: the interchanges of a spanning tree, in any order, turn $\psi$ into a tour.
5. Lemma 2: some minimal cost spanning tree of $G_\varphi$ uses only arcs $R_{i,i+1}$.
6. Lemma 5: adjacent interchanges executed on $\varphi$ in the stated order have additive cost.
7. Theorem 3: $\psi^*$ is a tour of cost $c(\varphi)+c_\varphi(\tau)$.
8. Theorem 4: $c(\psi)\ge c(\varphi)+c^*(\psi)$ for every permutation, with the underestimate $c^*$ of (17).
9. Lemma 7: for a tour $\psi$ the graph $G_\psi^*$ is connected.
10. Lemma 8: conditions (22a) and (22b) hold for equally many indices.
11. 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