Graph Theory

Motivation

Scheduling unrelated parallel machines to minimize the makespan, written $R\,\|\,C_{\max}$, is one of the basic NP-hard problems of scheduling theory. A set of jobs must each be run on one of several machines, and the time a job takes depends arbitrarily on the machine; the goal is to finish all jobs as early as possible. Before the work formalized here, the best polynomial algorithm known guaranteed only a schedule within $2\sqrt m$ times the optimum (Davis and Jaffe, 1981), a factor that grows with the number of machines $m$.

Lenstra, Shmoys and Tardos (FOCS 1987; CWI Report OS-R8714, 1987; Math. Programming 46, 1990) gave a polynomial algorithm with guarantee $2$, independent of $m$. Their tool is a rounding theorem: a vertex of a natural linear-programming relaxation can be rounded to an integral schedule that exceeds each machine's budget by at most one job. The rounding theorem and the binary-search framework around it became standard material in approximation algorithms.

Setting

There are $n$ jobs and $m\ge 1$ machines. If job $j$ is scheduled on machine $i$, it takes $p_{ij}$ time units, a positive integer. A schedule $\sigma$ assigns every job $j$ to one machine $\sigma(j)$. The load of machine $i$ is $\sum_{j:\sigma(j)=i}p_{ij}$, the makespan of $\sigma$ is the largest load, and $\mathrm{OPT}$ is the minimum makespan over all schedules.

For deadlines $d_1,\dots,d_m$ and a threshold $t$, let $J_i(t)=\{j: p_{ij}\le t\}$ and $M_j(t)=\{i : p_{ij}\le t\}$. The linear program (LP) has variables $x_{ij}\ge 0$ for $j\in J_i(t)$ and constraints

$$\sum_{i\in M_j(t)}x_{ij}=1\quad(j=1,\dots,n),\qquad \sum_{j\in J_i(t)}p_{ij}x_{ij}\le d_i\quad(i=1,\dots,m).$$

The integer program (IP) replaces $d_i$ by $d_i+t$ and requires $x_{ij}\in\{0,1\}$. A vertex of (LP) is an extreme point of its feasible polytope. The support graph of a point $\tilde x$ is the bipartite graph on machines and jobs with an edge $(i,j)$ whenever $\tilde x_{ij}>0$.

A $\rho$-relaxed decision procedure answers, for a deadline $d$, either 'no' or a schedule, such that (1) every schedule it returns has makespan at most $\rho d$, and (2) if it answers 'no', no schedule has makespan at most $d$. The binary search of Lemma 1 starts from the greedy schedule (each job on a machine where it runs fastest), whose makespan $t$ is an upper bound $u$, with lower bound $l=\lceil t/m\rceil$, queries the procedure at $d=\lfloor(u+l)/2\rfloor$, moves $u$ to $d$ on a schedule and $l$ to $d+1$ on 'no', and outputs the best schedule found once $l=u$.

The LP rounding procedure answers, on deadline $d$, by solving (LP) with $d_1=\dots=d_m=t=d$: 'no' if it is infeasible, and otherwise a 0-1 solution of (IP) obtained by rounding a vertex $\tilde x$ chosen by the LP solver, supported on $\tilde x$.

Formalization targets

Goal: Theorem 2

For every LP solver (every rule choosing a vertex of (LP) when it is feasible), an LP rounding procedure $D$ exists, and for every such $D$ the output $\sigma_D$ of the binary search satisfies

$$\operatorname{makespan}(\sigma_D)\le 2\cdot\mathrm{OPT}.$$

Milestones

1. The support graph of every vertex of (LP) is a pseudoforest: every set $S$ of machines and $T$ of jobs spans at most $|S|+|T|$ edges (§2, p. 4).
2. In a machine–job pseudoforest, every set of jobs of degree at least $2$ can be matched injectively into the machines (§2, pp. 4–5).
3. A schedule supported on a feasible $\tilde x$ with at most one fractional job per machine has loads at most $d_i+t$ (§2, p. 5).
4. Theorem 1 (Rounding Theorem): every vertex $\tilde x$ of (LP) has a schedule $\sigma$ supported on $\tilde x$ with

$$\sum_{j:\sigma(j)=i}p_{ij}\le d_i+t\qquad(i=1,\dots,m).$$

5. Lemma 1: for every $\rho$-relaxed decision procedure, the binary search outputs a schedule of makespan at most $\rho\cdot\mathrm{OPT}$.
6. A schedule with makespan at most $d$ gives a feasible point of (LP) with $d_i=t=d$ (§3, p. 5).
7. The LP rounding procedure is $2$-relaxed (§3, pp. 5–6).

Significance

Theorem 2 gives a constant-factor approximation for $R\,\|\,C_{\max}$ that does not depend on $m$. The same rounding theorem drives the paper's second algorithm, a $(1+\epsilon)$-approximation for a fixed number of machines using polynomial space, and the paper's lower bound shows that no polynomial algorithm achieves a factor below $3/2$ unless $\mathrm{P}=\mathrm{NP}$. The Rounding Theorem, in its later form for generalized assignment by Shmoys and Tardos (1993), is a standard tool for LP-based scheduling and assignment.

The result is proved; it has, to our knowledge, no machine-checked proof. The platform contains Matoušek and Gärtner's textbook version (MatousekLP.Scheduling.lst_two_approximation, Theorem 8.3.4 of Understanding and Using Linear Programming), which uses a different relaxation: one bound minimized parametrically over $T$, optimal solutions with linearly independent columns, and no per-machine deadlines. This mission formalizes the report's own route: deadlines $d_i$, arbitrary vertices, binary search over a relaxed decision procedure. A formal proof would also yield reusable statements about extreme points of transportation-type polytopes and matchings in pseudoforests.

Difficulty

The obvious rounding, putting each job on a machine where $\tilde x_{ij}$ is largest, can overload a machine by many jobs at once: nothing in feasibility alone prevents many jobs from each placing a small fraction on the same machine. The bound $d_i+t$ requires that each machine receive at most one job that the vertex treats fractionally, and this fails for general feasible points; it holds only because $\tilde x$ is a vertex. The step that carries the weight is therefore a statement about the combinatorial structure of the support of an extreme point, which must be derived from the linear independence of the tight constraints, followed by a matching argument on the resulting graph. Neither step is available in Mathlib in the form needed.

On the algorithmic side, the binary search must be shown to return a schedule within $\rho\cdot\mathrm{OPT}$ although the decision procedure is only approximately correct; the invariants (the lower bound stays below $\mathrm{OPT}$, the stored schedule stays within $\rho$ times the upper bound) have to be tracked through a recursion.

Formalization scope

• Machines are Fin m, jobs Fin n, processing times a matrix P : Matrix (Fin m) (Fin n) ℕ with all entries positive in Lemma 1 and Theorem 2 (the paper's model, p. 2). Loads, makespans and optimal schedules are the published MatousekLP.Scheduling.Schedule definitions applied to the real matrix $(p_{ij})$; $\mathrm{OPT}$ is the makespan of a schedule σopt with IsOptimalSchedule.
• (LP) is modelled on full $m\times n$ real matrices with the entries $p_{ij}>t$ fixed to $0$; this polytope is affinely isomorphic to the paper's, so vertices (Mathlib's Set.extremePoints) correspond exactly. Theorem 1 and its steps are stated for real deadlines and real $t\ge 0$, more general than the paper's integers; the paper's proof does not use integrality, and mission 2 of this series needs non-integral $t$.
• Algorithmic wording not formalized. Theorem 2 states "a 2-approximation algorithm ... that runs in time bounded by a polynomial in the input size"; Lemma 1 speaks of polynomial procedures; Theorem 1 adds "this rounding can be done in polynomial time". Running time, the ellipsoid method and vertex finding are not formalized. What is formalized is the guarantee the proofs establish: the binary search, written as a Lean function, returns a schedule within $\rho\cdot\mathrm{OPT}$ (Lemma 1, for every $\rho$-relaxed procedure) and within $2\cdot\mathrm{OPT}$ for every LP rounding procedure and every choice of vertex (Theorem 2).
• Explicit constants: the factor $2$ of Theorem 2 and of the $2$-relaxed procedure, which comes from $d_i+t$ with $d_i=t=d$; the overshoot $t$ of Theorem 1; the initial bounds $u=$ greedy makespan and $l=\lceil u/m\rceil$ (the paper's $t/m$, rounded up because $\mathrm{OPT}$ is an integer); the query point $\lfloor(u+l)/2\rfloor$.
• The LP solver's choice is quantified over by a vertex selector, returning a vertex when (LP) is feasible and nothing otherwise; one always exists, since the polytope is compact.
• Trivializing formalization ruled out. "There is a schedule with makespan at most $2\cdot\mathrm{OPT}$" is trivially witnessed by an optimal schedule; the goal instead bounds the output of the binary search, whose every 'almost' answer must be a rounding of the solver's vertex, supported on it and feasible for (IP).
• Needed infrastructure: extreme points of polytopes given by linear constraints and their tight-constraint rank characterization; bipartite pseudoforests and Hall-type matchings; well-founded recursion for the search. Proofs of any milestone, and reusable lemmas on extreme points of assignment polytopes, are welcome.

Selected references

• J. K. Lenstra, D. B. Shmoys, É. Tardos, Approximation algorithms for scheduling unrelated parallel machines, CWI Report OS-R8714, Centre for Mathematics and Computer Science, Amsterdam, 1987 (the source of this mission's statements and numbering); also Proc. 28th IEEE Symposium on Foundations of Computer Science (1987) 217–224
• J. K. Lenstra, D. B. Shmoys, É. Tardos, Approximation algorithms for scheduling unrelated parallel machines, Mathematical Programming 46 (1990) 259–271, https://doi.org/10.1007/BF01585745
• E. Davis, J. M. Jaffe, Algorithms for scheduling tasks on unrelated processors, Journal of the ACM 28 (1981) 721–736, https://doi.org/10.1145/322276.322284
• D. B. Shmoys, É. Tardos, An approximation algorithm for the generalized assignment problem, Mathematical Programming 62 (1993) 461–474, https://doi.org/10.1007/BF01585178
• J. Matoušek, B. Gärtner, Understanding and Using Linear Programming, Springer, 2007, §8.3, https://doi.org/10.1007/978-3-540-30717-4

Motivation

The restricted shortest path problem asks for a shortest route between two points of a network subject to a budget on a second additive quantity, such as travel time, cost or risk. It appears as the pricing subproblem of column generation for crew scheduling and vehicle routing, in quality-of-service routing in communication networks, and in scheduling, where Hassin's own §7 uses it for a single-machine problem. The problem is NP-hard (Garey and Johnson, 1979), so exact polynomial algorithms are not expected, and the natural question is how well it can be approximated in polynomial time.

Timeline.

• 1966–1985. Practical exact methods and pseudopolynomial dynamic programs (Joksch 1966; Lawler 1976; Handler and Zang 1980; Aneja, Aggarwal and Nair 1983; Henig 1985).
• 1987. Warburton gives the first fully polynomial approximation scheme (FPAS) for this problem on acyclic graphs, based on rounding and scaling (Warburton, Oper. Res. 35, 1987).
• 1992. Hassin gives two faster FPASs: a rounding-and-scaling scheme driven by an approximate decision test (§3–§4), and a strongly polynomial scheme (§5–§6) (Hassin, Math. Oper. Res. 17, 1992).
• 2001. Lorenz and Raz give a simpler and faster scheme built on the same test-and-search pattern (Lorenz–Raz, Oper. Res. Lett. 28, 2001).

Hassin's combination of an approximate decision test with a geometric search on the bounds is the pattern later schemes for resource-constrained path problems refine, which is why his first scheme is the subject of this mission.

Setting

A directed graph has vertex set $\{1,\dots,n\}$, $n\ge 2$, and edge set $E$. Following the paper, the vertices are numbered so that every edge $(i,j)\in E$ has $i<j$; in particular the graph is acyclic. Each edge carries a positive integer length $c_{ij}$ and a positive integer transition time $t_{ij}$. A path $p=(v_0,\dots,v_m)$ has length $c(p)=\sum_r c_{v_{r-1}v_r}$ and transition time $t(p)=\sum_r t_{v_{r-1}v_r}$. For a nonnegative integer $T$, a $T$-path is a path from $1$ to $n$ with $t(p)\le T$, and $\mathrm{OPT}$ is the length of a shortest $T$-path.

Fix $0<\varepsilon<1$. For a real $V$, the rounded lengths are

$$\tilde c^V_{ij}=\Big\lfloor \frac{c_{ij}(n-1)}{V\varepsilon}\Big\rfloor .$$

Procedure TEST(V) deletes the edges with $c_{ij}>V$ and answers NO if, for some integer $c<(n-1)/\varepsilon$, some $1$–$n$ path in the remaining graph has transition time at most $T$ and rounded length at most $c$; otherwise it answers YES.

The Rounding Algorithm keeps bounds $(LB,UB)$ on OPT. Starting from initial bounds $(LB_0,UB_0)$, Step 1 repeats while $UB>2LB$: with $V=(LB\cdot UB)^{1/2}$ it sets $LB\leftarrow V$ if TEST(V) = YES and $UB\leftarrow V(1+\varepsilon)$ if TEST(V) = NO. Step 2 outputs a $T$-path that is shortest for the rounded lengths $\tilde c^{LB}_{ij}=\lfloor c_{ij}(n-1)/(\varepsilon LB)\rfloor$. The bounds after $k$ passes are written $(LB_k,UB_k)$.

Formalization targets

Goal: the approximation guarantee of the Rounding Algorithm

If $LB_0>0$ is a lower bound on the length of every $T$-path, $N$ is a stage at which $UB_N\le 2LB_N$, and $p$ is a Step 2 output at $LB_N$, then

$$c(p)\le (1+\varepsilon)\,c(q)\qquad\text{for every }T\text{-path }q,$$

that is, $c(p)\le(1+\varepsilon)\,\mathrm{OPT}$. The initial upper bound $UB_0$ is arbitrary.

Milestones (§3–§4)

1. Rounding error (§3, p. 38): with $\delta=V\varepsilon/(n-1)$, $0\le c_{ij}-\delta\tilde c^V_{ij}\le\delta$ for every edge, and $0\le c(p)-\delta\tilde c^V(p)\le V\varepsilon$ for every path.
2. TEST(V) = NO (§3, p. 38): some $T$-path has length $<V(1+\varepsilon)$, so $\mathrm{OPT}<V(1+\varepsilon)$.
3. TEST(V) = YES (§3, p. 38): every $T$-path has length $\ge V$, so $\mathrm{OPT}\ge V$.
4. Bound update (§4, p. 39): along the run, $LB_k>0$ and $LB_k$ is a lower bound on every $T$-path; if some $T$-path has length at most $UB_0$, some $T$-path has length at most $UB_k$.
5. Scaled-optimum error (§4, p. 39): a Step 2 output $p$ at any $LB>0$ satisfies $c(p)\le c(q)+\varepsilon LB$ for every $T$-path $q$.

Companion statements

• Termination when $(1+\varepsilon)^2<2$: some stage $N$ has $UB_N\le 2LB_N$; and an explicit instance with $\varepsilon=9/10$ on which Step 1 never stops.
• Initial bounds (Step 0, p. 39): every $1$–$n$ path has length between $1$ and the sum of the $n-1$ longest edge-lengths.
• Algorithms A and B (§2, pp. 37–38): their recursions compute $f_j(t)$ and $g_j(c)$, with $\mathrm{OPT}=f_n(T)=\min\{c\mid g_n(c)\le T\}$.

Significance

The guarantee makes the Rounding Algorithm a fully polynomial approximation scheme: combined with the paper's running-time analysis, a $(1+\varepsilon)$-approximate $T$-path is computed in time polynomial in the input size and $1/\varepsilon$. The two ingredients, an approximate decision test that answers "OPT $\ge V$" or "OPT $<V(1+\varepsilon)$", and a geometric search on the ratio $UB/LB$, are reused in later FPASs for constrained path, knapsack-type and scheduling problems; the milestones isolate them as separate statements.

The result has been proved since 1992 but, as far as a search of the platform and of Mathlib shows, none of it is machine-checked. This mission produces a checked version of the first scheme, stated for every stage at which the printed stopping test holds and every optimal Step 2 output. It also records, as a companion, that the printed Step 1 need not terminate when $\varepsilon>\sqrt2-1$, and proves termination under $(1+\varepsilon)^2<2$.

Difficulty

The arithmetic of each step is short; the difficulty is in the combinatorial facts the page uses without proof and in the bookkeeping of a run. The rounding error of a path is at most $V\varepsilon$ only because a $1$–$n$ path has at most $n-1$ edges, which follows from the numbering $i<j$ and must be derived for list-encoded paths. The YES case must cover $T$-paths through edges that TEST deleted, which the rounding argument does not see. The bound update needs both bounds to stay positive so that $(LB\cdot UB)^{1/2}$ is a meaningful test point, an invariant of the whole run rather than of one step. A tempting shortcut, assuming that LB is a lower bound on OPT at the stopping stage, would assume milestone 4; the goal assumes it only for $LB_0$.

Formalization scope

• Representation. Vertices are natural numbers; an instance is a structure with $n$, a finite edge set of pairs, and length and time functions, with a well-formedness predicate: $n\ge 2$, every edge $(i,j)$ has $1\le i<j\le n$, and lengths and times are positive. The requirement $n\ge2$ is not printed: a $1$–$n$ path and the divisions by $n-1$ presuppose it. Paths are nonempty vertex lists.
• Arithmetic. $n-1$ is taken in the reals; $\lfloor\cdot\rfloor$ is the natural-number floor of a nonnegative real; $(LB\cdot UB)^{1/2}$ is the real square root. Bounds and $\varepsilon$ are reals, $T$ is a natural number.
• OPT. OPT is never a number in the formal statements, because it is $\infty$ when no $T$-path exists. "OPT $\ge V$" is a bound on every $T$-path, "OPT $<V(1+\varepsilon)$" is the existence of a $T$-path, and the goal compares the output with every $T$-path. Algorithms A and B use values in $\mathbb N\cup\{\infty\}$.
• TEST(V) is defined by the answer the procedure reaches, not through Algorithm B's printed recursion, whose initial condition $g_j(0)=\infty$ is wrong for rounded lengths $0$; for $n\ge2$ and $\varepsilon<1$ the answers agree.
• The run is the iterate of one pass of Step 1; a stopped state is a fixed point. Step 2 outputs any $T$-path optimal for the rounded lengths, without pruning edges, as printed.
• Added hypothesis. The termination statement assumes $(1+\varepsilon)^2<2$, which the page does not state; without it the printed loop can run forever, and an explicit instance is included.
• Not a trivialization. The goal assumes nothing about TEST's correctness, the rounding error or the lower-bound invariant along the run, and the termination companion shows that its stopping hypothesis is reachable.
• Out of scope. The second, strongly polynomial scheme of §5–§6 is not included, because as printed its Partitioning Algorithm can report infeasibility on a feasible instance and formalizing it would require a corrected algorithm that is not the author's. All running-time claims, stated as $O(\cdot)$ bounds under an informal operation count, are also excluded, as are the $V'$ variant of the test points and the scheduling application of §7.
• Reusable parts. The list-based path layer with two additive weights, and the correctness of the pseudopolynomial recursions of Algorithms A and B, are independent of the approximation scheme. Contributions of proofs for any milestone or companion are welcome.

Selected references

• R. Hassin, Approximation schemes for the restricted shortest path problem, Mathematics of Operations Research 17(1):36–42, 1992. https://doi.org/10.1287/moor.17.1.36
• A. Warburton, Approximation of Pareto optima in multiple-objective, shortest-path problems, Operations Research 35(1):70–79, 1987. https://doi.org/10.1287/opre.35.1.70
• D. H. Lorenz and D. Raz, A simple efficient approximation scheme for the restricted shortest path problem, Operations Research Letters 28(5):213–219, 2001. https://doi.org/10.1016/S0167-6377(01)00069-4
• M. R. Garey and D. S. Johnson, Computers and Intractability: A Guide to the Theory of NP-Completeness, W. H. Freeman, 1979.

Motivation

PERT (Program Evaluation and Review Technique) and the critical path method model a project as a directed acyclic network whose arcs are jobs and whose nodes are events; the duration of the project is the length of a longest path from the origin to the terminal. When job durations are random, the quantity a planner wants is the expected duration. Computing it exactly requires solving one longest-path problem for every joint outcome of the job durations: with $m$ jobs each taking two values, $2^m$ deterministic problems. Classical PERT practice replaced every random duration by its mean and reported the longest path for the mean durations. That figure is known to be optimistically biased.

D. R. Fulkerson, Expected Critical Path Lengths in PERT Networks (RAND Memorandum RM-3075-PR, 1962; Operations Research 10(6):808–817, 1962, doi:10.1287/opre.10.6.808), proposed a second estimate, computed node by node with work exponential only in the size of a single node's bundle of incoming arcs, and proved that it lies between the classical mean-length figure and the true expectation.

Setting

A project network has events $0,1,\dots,n$ with $n\ge1$, origin $0$ and terminal $n$. Its arcs are ordered pairs $(i,j)$ with $i<j$, at most one per pair, and every event lies on a directed path from the origin to the terminal. Fulkerson numbers his nodes $1,\dots,n$; his node $i$ is event $i-1$ here. The bundle $B_j$ of an event $j$ is the set of arcs entering $j$, and $\operatorname{pred}(j)$ the set of their tails; the origin's bundle is empty.

For arc lengths $t$, let $\ell_i(t)$ be the length of a longest (critical) path from the origin to $i$; equivalently $\ell_0=0$ and $\ell_j=\max_{i\in\operatorname{pred}(j)}(\ell_i+t_{ij})$.

The lengths of the arcs of each bundle $B_j$ form a random vector with a finite distribution: a finite set $S_j$ of bundle vectors $v$, where $v_i$ is the length of arc $(i,j)$, with probabilities $p_j(v)\ge 0$ summing to $1$. Arcs within a bundle may be correlated; distinct bundles are independent, so an assignment $\omega=(\omega_j)_j$ of one bundle vector per event has probability $p(\omega)=\prod_j p_j(\omega_j)$. Three numbers are attached to each event $i$:

1. the expected critical path length $e_i=\sum_\omega p(\omega)\,\ell_i(t(\omega))$;
2. the mean-length estimate $g_i=\ell_i(\bar t)$, where $\bar t_{ij}=\sum_{v\in S_j}p_j(v)\,v_i$ is the expected length of arc $(i,j)$;
3. Fulkerson's numbers $f_0=0$ and, for $j\neq0$,

$$f_j=\sum_{v\in S_j}p_j(v)\,\max_{i\in\operatorname{pred}(j)}\bigl(f_i+v_i\bigr).$$

Formalization targets

Goal: (4.4)

$$g_i\;\le\;f_i\;\le\;e_i\qquad\text{for every event } i .$$

Milestones

In the order of Fulkerson's induction (pp. 10–12):

1. the recursion for $\ell$ computes the greatest path length (§3, (3.6), and the display on p. 11);
2. $\ell_i(t)$ depends only on the arcs of the bundles $B_0,\dots,B_i$ (p. 6);
3. (4.8): $\max_{i\in\operatorname{pred}(j)}(f_i+\bar t_{ij})\le f_j$;
4. (4.5)/(4.9): if $g_k\le f_k$ for all $k<j$, then $g_j\le f_j$;
5. (4.13): $\sum_{v\in S_j}p_j(v)\max_{i\in\operatorname{pred}(j)}(e_i+v_i)\le e_j$;
6. (4.10)/(4.14): if $f_k\le e_k$ for all $k<j$, then $f_j\le e_j$.

Companion statements

• $g_i\le e_i$ under an arbitrary joint distribution of all arc lengths (remark, p. 12).
• Fig. 4.2: with correlated bundles, $e_3=g_3=1$ but $f_3=5/4$, so (4.4) fails without bundle independence.
• (4.17): an independent example with $g_3=f_3=1<e_3=5/4$.
• Fig. 4.1: explicit values $g_4=3/2$, $f_2=1/2$, $f_3=9/8$, $f_4=55/32$, and $f_i=e_i$.

Significance

The chain (4.4) says that the classical PERT estimate $g$ never overstates the expected project duration, and that the numbers $f$ are a lower bound at least as tight. The $f$ computation visits each node once and sums over the support of that node's bundle only, so its cost grows exponentially with bundle size rather than with network size, while the exact expectation $e$ requires the whole product space. The Fig. 4.2 example shows that the bundle-independence hypothesis cannot be dropped for the upper inequality, while the lower inequality $g\le e$ survives arbitrary dependence.

The result has a complete published proof. This mission seeks a machine-checked proof of (4.4) for finite distributions, with the longest-path characterisation of the earliest-event-time recursion and the locality of critical path lengths as reusable lemmas, and machine-checkable versions of the paper's numerical examples, including the counterexample showing the role of independence.

Difficulty

The left inequality compares an average of maxima with a maximum of averages. The right inequality requires more: $f_j$ averages over the bundle entering $j$, while $e_j$ averages over assignments to every bundle. Taking expectations in $\ell_j=\max_i(\ell_i+t_{ij})$ yields $e_j\ge\max_i(e_i+\bar t_{ij})$, which gives the weaker bound $g\le e$. Fig. 4.2 shows that $f\le e$ can fail when the bundles are dependent. In Lean, $e$ is a sum over a dependent product of finite supports (Fintype.piFinset); its interaction with the local recurrence for $f$ is the central technical difficulty.

Formalization scope

• Network: the published CriticalPath.Events.ProjectNetwork (Kelley–Walker 1959): events Fin (n + 1), arcs a Finset of ordered pairs with strictly increasing labels, origin preceding and terminal following every event. This requires $n\ge1$. Fulkerson's numbering condition "$i\le j$" on p. 3 is read as the strict $i<j$ (arcs join distinct nodes of an acyclic network). There is one arc per ordered pair, Fulkerson's own convention in (3.13).
• Critical path length: the published CriticalPath.Events.earliest, a recursion with Finset.sup' over the nonempty set of incoming arcs. This is the paper's convention that terms of missing arcs are ignored. Nothing uses a default value of $0$ or $-\infty$.
• Distributions: finite, given as data (a support Finset and a weight function per bundle) plus a predicate IsProb (nonnegative weights on the support, summing to $1$, for every event including the origin). Bundle vectors are functions on all events, and coordinates outside $\operatorname{pred}(j)$ are never read.
• Arc lengths are arbitrary reals. §3 assumes nonnegative lengths, but its footnote on p. 4 states that nonnegativity "is not essential in this or the following section"; the statements are given in this more general form.
• No trivialization: $e_i$ is the sum over every assignment of bundle vectors, weighted by the product probability (3.5). It is not defined by a recursion, and the goal assumes none of the milestones. $f$ at node $j$ uses only the distribution of the bundle of $j$.

Infrastructure that a full development needs, and that is reusable elsewhere, includes the longest-path characterisation of the earliest-event-time recursion, the locality lemma, and the factorisation of sums over Fintype.piFinset along one coordinate. Proofs of any milestone or companion are welcome. Out of scope here: §5 (computational examples) and the general-network analogues of §6.

Selected references

• D. R. Fulkerson, Expected Critical Path Lengths in PERT Networks, RAND Memorandum RM-3075-PR, March 1962; published in Operations Research 10(6):808–817, 1962. doi:10.1287/opre.10.6.808
• J. E. Kelley Jr. and M. R. Walker, Critical-Path Planning and Scheduling, Proceedings of the Eastern Joint Computer Conference, 1959, pp. 160–173. doi:10.1145/1460299.1460318
• D. G. Malcolm, J. H. Roseboom, C. E. Clark and W. Fazar, Application of a Technique for Research and Development Program Evaluation, Operations Research 7(5):646–669, 1959. doi:10.1287/opre.7.5.646

Motivation

A postal route that must traverse every street and return to its starting point is a Chinese postman tour. In a street network, crossings are nodes, streets are edges, and the cost of a route is the sum of the lengths of the streets it traverses, counted with repetition. The practical question is which streets must be repeated, and how often. Edmonds and Johnson's 1973 paper separates that question from constructing the resulting tour: choose the repeated edges first, then find an Euler tour of the resulting multigraph. This mission concerns their reduction of the first question to a minimum-weight matching of the odd-degree nodes.

The reduction matters because it turns a route problem with arbitrary repeated edge traversals into a finite pairing problem. The graph of odd nodes is complete, with the weight of a pair given by its shortest-path distance in the original network. A matching chooses which odd nodes to pair, and paths realizing those pairs identify edges to repeat. The paper also explains why overlapping paths can be replaced so that no edge needs to be repeated by this construction more than once (§3, pp. 92–93).

Setting

A graph $G=(N,E)$ has finite node and edge sets. Each edge has two distinct endpoints. Different edges may join the same pair of nodes, so parallel streets remain distinct. The graph is connected when every pair of nodes is joined by an edge-labelled walk. A walk records both its node sequence and its edge sequence; a tour is a closed walk. An Euler tour uses each edge exactly once, while a postman tour uses each edge at least once. Edge lengths $c_e$ are real and nonnegative, as in §2, p. 89.

The degree of $v$ is the number of named edges meeting it. Let $T$ be the set of nodes of odd degree. For every edge $e$, let $x_e\in\mathbb N$ be the number of additional traversals. The parity equations require a nonnegative integer $w_v$ at each node such that

$$\sum_{e\ni v}x_e=2w_v+b_v,\qquad b_v=\begin{cases}1&v\in T,\\0&v\notin T.\end{cases}$$

Their objective is $z(x)=\sum_{e\in E}c_ex_e$. These are the paper's (3.1)–(3.4), with natural-number values encoding integrality and nonnegativity (§3, pp. 90–91). The equations express the even-degree condition after adding $x_e$ copies of each original edge.

For nodes $u,v$, write $d(u,v)$ for the length of a shortest path in $G$. This distance is backed by an attaining edge-simple path and is a lower bound on the length of every walk from $u$ to $v$. Connectivity and nonnegative edge lengths make that specification meaningful. Let $G_p$ be the complete graph on $T$, with edge $\{u,v\}$ of weight $d(u,v)$. A 1-matching $M$ pairs every node of $T$ with exactly one distinct node. Its length is $L(M)=\sum_{\{u,v\}\in M}d(u,v)$, equivalently half the sum of $d(v,f(v))$ over $v\in T$ for the pairing involution $f$ (§3, p. 92).

Formalization targets

Odd-node matching reduction

The goal asserts the existence of a 1-matching of the odd nodes and both directions of the cost comparison:

$$\forall M\;\exists x\text{ satisfying the parity equations}:\quad x_e\in\{0,1\},\ z(x)\le L(M),$$ $$\forall x\text{ satisfying the parity equations}\;\exists M:\quad L(M)\le z(x).$$

The existence conclusion and these comparisons identify the two attained minimum values. The goal does not prescribe a particular matching algorithm. Its supporting targets are the paper's uncrossing of overlapping shortest paths, parity of their union, reduction of multiplicities to zero or one, and decomposition of a parity solution into paths between odd nodes (§3, pp. 92–93).

Postman-tour reduction

The companion target relates a tour's edge counts to the parity equations. A postman tour traverses edge $e$ exactly $1+x_e$ times, and its length is

$$\sum_{e\in E}c_e(1+x_e) =\sum_{e\in E}c_e+z(x).$$

Conversely, positive integer edge counts with even incidence at every node can be ordered into a postman tour of a connected graph. The supporting Euler theorem handles a connected even multigraph (§2, p. 89).

Significance

The matching result characterizes the optimal additional cost of an undirected postman route. It says that the parity correction can be chosen from paths pairing odd nodes, and that no feasible choice of repeated traversals can beat the best such pairing. The companion identifies how that correction becomes an actual tour. The distinction is useful when one wants to change the matching method while retaining the mathematical guarantee on route length.

A formal development would provide a reusable account of finite multigraph walks whose edge names distinguish parallel edges, of shortest-path distances with explicit attainment, and of parity subgraphs decomposed into odd-to-odd paths and even-degree residual tours. These pieces support later formal work on route inspection, $T$-joins, and matching-based graph algorithms. The paper proves the mathematical result. The exact multigraph and cost statements drafted here are open formalization targets; the local prior-art search found related results for simple graphs and metric traveling-salesman models, but no published statement with this paper's objects and conclusion.

Difficulty

A direct shortest-path construction can assign the same original edge to two matching pairs. Simply setting $x_e=1$ for the union then loses the additivity of path lengths, and setting $x_e=2$ loses the promised zero-or-one form. The uncrossing claim must control both the matching cost and the number of times each original edge appears. In the converse direction, an arbitrary feasible $x$ may contain repeated edges and cycles; the argument must account for these without assuming that every supported edge belongs to a path between odd nodes (§3, pp. 92–93).

Formalization scope

Lean uses the published EdmondsMatching65.Polyhedron.Graph for $G$: finite node and edge types and an endpoint map into unordered node pairs. A proof field excludes loops; distinct edge names may have identical endpoints. Walks use lists of nodes and named edges with zero-based indices, and the one-node, zero-edge walk is allowed. Edge multiplicities and parity witnesses are natural numbers. Costs and shortest-path lengths are real. The distance relation requires both an attaining edge-simple path and a bound against all walks; no real infimum over a possibly empty family is used. The matching is a fixed-point-free involution on the odd nodes, extended by the identity elsewhere, and each pair contributes half of its two directed distance terms.

The goal assumes a connected graph and nonnegative edge lengths, exactly as the section does. The tour-only results require a nonempty node type because a list-based tour must have a starting node; without it an edgeless graph on no nodes would satisfy connectivity and even degree vacuously. The path-decomposition statement permits unused even-degree cycles. No independent set of “odd nodes” is accepted as input: it is computed from the degree of $G$.

The development needs finite multigraph incidence, edge-labelled walks, shortest paths, finite matchings, parity arithmetic, path uncrossing, and Euler tours. Proofs or useful intermediate results for these objects are welcome, including results applicable to multigraphs beyond the postman setting.

Selected references

• Jack Edmonds and Ellis L. Johnson, Matching, Euler tours and the Chinese postman, Mathematical Programming 5 (1973), 88–124. DOI: 10.1007/BF01580113.

Motivation

The Chinese postman problem asks for a shortest closed walk in a graph that traverses every edge at least once. Edmonds and Johnson (Math. Programming 5 (1973) 88–124) reduce it to two subproblems: choosing, by matching, which edges to duplicate so that every node has even degree, and then actually finding an Euler tour of the resulting even graph, a closed walk using every edge exactly once. Euler's theorem guarantees such a tour exists in a connected even graph, but an algorithm has to produce one and represent it compactly.

Section 5 of the paper gives two such representations and two algorithms. This mission formalizes the next-node representation: for each node $n$, a list of the nodes the tour goes to when leaving $n$. Theorem 5.1, which the paper attributes to its reference [1] (van Aardenne-Ehrenfest and de Bruijn, 1951) and to Berge's textbook, characterises exactly which lists describe an Euler tour; Theorem 5.2 shows the paper's next-node algorithm produces such lists. The same correspondence between Euler tours and arborescences is the combinatorial core of the BEST theorem on counting Euler tours of directed graphs (van Aardenne-Ehrenfest and de Bruijn, 1951).

Setting

A graph $G$ is a finite set of nodes and a finite set $E$ of edges, each edge meeting two distinct nodes; several edges may meet the same pair of nodes. The degree $\deg(n)$ counts the edges meeting $n$, and $\#(n,m)$ counts the edges meeting both $n$ and $m$. A tour is an alternating sequence $(n_1, e_1, n_2, \dots, e_l, n_{l+1} = n_1)$ in which $e_i$ meets $n_i$ and $n_{i+1}$; an Euler tour contains every edge exactly once. $G$ is connected when every two nodes are joined by such a sequence, and even when every degree is even.

Next-node lists assign to each node $n$ a list $L_n(1), \dots, L_n(k_n)$ of nodes. Given a starting node $r$, the lists specify a walk: start at $r$; the first time a node $n$ is reached (for $r$, at the start), leave it to $L_n(k_n)$; the second time, to $L_n(k_n - 1)$; and so on, so the lists are read from the last entry to the first. The walk stops at the first node whose list is used up. The lists describe an Euler tour when this walk uses every entry of every list and its node sequence is the node sequence of an Euler tour of $G$. With parallel edges, the lists name nodes only, and the edge used at each step is chosen so that every edge is used once.

An arborescence with root $r$ is a tree whose edges are directed so that every node $n \ne r$ has exactly one edge directed away from it, and $r$ has none.

Formalization targets

Goal: Theorem 5.1 (p. 112)

For any node $r$ of an even, connected graph $G$, next-node lists describe an Euler tour from $r$ if and only if

$$\text{(i)}\ k_n = \tfrac12\deg(n)\ \ \forall n,\qquad \text{(ii)}\ \#(n,m) = |\{i : L_m(i) = n\}| + |\{i : L_n(i) = m\}|\ \ \forall n, m,\qquad \text{(iii)}\ \{\,n \to L_n(1) : n \ne r\,\}\ \text{is an arborescence with root } r .$$

The printed condition (iii) names the edges $(n, L_n(k_n))$; the paper's own proofs of Theorems 5.1 and 5.2 use $(n, L_n(1))$, the last exit from $n$, and the printed version is false on a five-edge example. The goal states $L_n(1)$.

Milestones

The proof on pp. 112–113 splits into five claims, each a milestone:

1. an Euler tour's lists satisfy (i) and (ii);
2. every node set $S$ with $r \notin S$ has a last-exit edge $n \to L_n(1)$ leaving it;
3. a map with one outgoing edge per node $n \ne r$ and an edge leaving every set avoiding $r$ is an arborescence;
4. under (i) and (ii) the walk from $r$ returns to $r$ having traversed every edge meeting $r$;
5. at that point every node $n$ incident to an untraversed edge differs from $r$ and still has its last exit $L_n(1)$ unused.

Companion: Theorem 5.2 (p. 112)

The lists produced by any complete run of the next-node algorithm of §5.2 satisfy (i), (ii) and (iii); together with Theorem 5.1, they describe an Euler tour.

Significance

Theorem 5.1 replaces a global property, that a walk uses each edge exactly once, by three local checks: list lengths, pair counts, and a tree condition on one distinguished entry per node. That is what makes the next-node representation usable. An algorithm only has to build lists with (i)–(iii), and Theorem 5.2 shows the paper's algorithm does so for every nondeterministic choice it makes. The same arborescence condition counts Euler tours in the BEST theorem: each arborescence and each ordering of the remaining exits gives a distinct tour.

The results have been proved since 1951. What this mission proposes is a Lean formalization on multigraphs with parallel edges, which is the setting the Chinese postman reduction needs, since duplicated edges are parallel. A search of Mathlib and of the platform finds no formalization of Theorem 5.1, of next-node lists, or of arborescences in this form. Mathlib has Eulerian walks only for simple graphs, and the existing platform statements of Euler's theorem (for example SupplyChainTheory.euler_tour_iff) are about simple graphs and existence only.

Difficulty

The necessity of (i) and (ii) is counting. The substance is in two places.

First, necessity of (iii): the last exits must be shown to leave every set avoiding $r$. The tempting choice of the first exits $L_n(k_n)$, which is what the theorem's printed text says, is wrong: on an Euler tour the first exits can form a cycle, so any argument that does not distinguish first from last exits cannot work.

Second, the converse: a walk that follows lists satisfying only (i) and (ii) can return to $r$ early and leave edges untraversed, so (iii) is indispensable, and the statement depends on exactly which list entries have been used when the walk stops. Making that bookkeeping precise for a walk defined by a counter per node, and turning the used entries into an actual edge sequence in a multigraph, is the main formal work. For Theorem 5.2 the difficulty is the invariant of a nondeterministic algorithm: every trail it starts closes at its starting node because the graph is even.

Formalization scope

All declarations live in the namespace ChinesePostman.NextNode. A graph is a local ChinesePostman.NextNode.Graph V E structure on finite types: ends : E → Sym2 V and a proof that no edge is a loop, so parallel edges are distinct elements of E with the same ends. Walks are pairs of a node list and an edge list. A list $L_n$ is a Lean List V, so $L_n(i)$ is the entry at index $i-1$ and $k_n$ is the length. The walk specified by the lists is computed by follow L r, a fuel-bounded iteration whose state is the current node and the number of departures made from each node. It returns the node sequence and the final counters. DescribesEulerTour G r L requires every counter to reach the list length and some edge list to make the node sequence an Euler tour. Condition (ii) is quantified over all pairs including $n = m$, where it forbids a node in its own list. Condition (iii) requires every list of a node $n \ne r$ to be nonempty, its chosen exit to be an edge of $G$, and requires the iterates of the parent map $n \mapsto L_n(1)$ (with $r \mapsto r$) to reach $r$ from every node. The next-node algorithm is an inductive step relation on states, and "produced" means reachable termination from the Step 0 state.

Added hypotheses: Theorem 5.2 and its corollary assume an edge $e_0$ meeting $r$, which Step 0 needs; a one-node graph without edges satisfies Theorem 5.1 trivially and is not excluded. Milestones drop the hypotheses their claims do not use (connectivity, evenness), which makes them stronger.

A trivializing formalization is ruled out explicitly: the lists are read backwards, from $L_n(k_n)$ to $L_n(1)$, and must all be used up. Reading them forwards, dropping the "uses every entry" clause, or stating (iii) with an empty-list default for the parent would each make a different, and in some cases false, statement.

The development needs walks on multigraphs, counting arguments for closed walks (in-degree equals out-degree along the walk), and a finite pigeonhole/orbit argument for the arborescence. The arborescence lemma (milestone 3) is graph-free and reusable. Proofs of any milestone, and of the multigraph walk lemmas they need, are welcome.

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 (reference [1] of the paper, cited there as "Circuits and trees in oriented graphs").
• C. Berge, The Theory of Graphs and its Applications, Wiley, New York, 1962 (reference [3] of the paper).

Motivation

Minimum-cost circulation asks how to route flow around a directed network without accumulating flow at any vertex, while minimizing the total cost of the routed units. It is a basic network optimization problem: lower-bound and demand constraints in many flow models can be converted into circulation form. Goldberg and Tarjan's 1987 technical report develops a successive-approximation approach in which a local repair subroutine, refine, improves an approximately optimal circulation. The report was followed by a 1990 journal article; all theorem numbers and page citations in this mission refer to the 1987 report.

The mission isolates the generic form of refine, where an implementation may choose any applicable update at each step. Its question is whether every such choice sequence finishes after a controlled number of operations and returns a circulation with a stronger optimality certificate. The related Goldberg–Tarjan maximum-flow algorithm uses push and relabel operations with distance labels; here the labels are real-valued prices tied to arc costs. The authors' cycle-canceling work uses the same circulation network model and supplies published definitions reused in this development.

Setting

A circulation network has a finite vertex set $V$ and a symmetric set $E$ of directed arcs: whenever $(v,w)$ is an arc, so is $(w,v)$. Let $n=|V|$ and $m=|E|$, counting both orientations. Each arc has a real capacity $u(v,w)$ and cost $c(v,w)$, with $c(v,w)=-c(w,v)$. A pseudoflow $f$ respects capacities and the paired-arc relation $f(v,w)=-f(w,v)$. Its excess $e_f(v)$ is the sum of flow entering $v$. A circulation is a pseudoflow with zero excess everywhere. The already published CycleCanceling.MinMean.Network supplies this network, its circulation predicate, and residual capacity $u_f(v,w)=u(v,w)-f(v,w)$. An arc is residual when this capacity is positive.

A price function $p:V\to\mathbb R$ changes an arc's reduced cost to $c_p(v,w)=c(v,w)-p(v)+p(w)$. A pseudoflow is $\varepsilon$-optimal with respect to $p$ when every residual arc has reduced cost at least $-\varepsilon$. A vertex is active when its excess is positive. An admissible arc is a residual arc of negative reduced cost. Refine takes an input circulation that is $2\varepsilon$-optimal, saturates every arc whose reduced cost is negative, and then repeatedly applies an available update. A push sends flow from an active vertex along an admissible arc. A relabel raises the price of an active vertex with no outgoing admissible arc to the largest value permitted by $\varepsilon$-optimality. These rules are Figures 4 and 5, printed pages 18–19.

Formalization targets

The supporting targets are the paper's progress and correctness results, its price bound, and the three operation counts. For any generic refine run from a $2\varepsilon$-optimal circulation, Lemma 5.8 bounds each vertex's price increase by $3n\varepsilon$. Lemmas 5.9–5.11 bound the numbers $R,S,T$ of relabelings, saturating pushes, and nonsaturating pushes:

$$R\leq 3n(n-1),\qquad S\leq 3nm,\qquad T\leq 3n^2(m+n).$$

The goal combines the resulting bound on the number $K$ of updates with progress and correctness:

$$K\leq 3n(n-1)+3nm+3n^2(m+n).$$

If the final state has an active vertex, another update exists. If no update applies, the final pseudoflow is a circulation and is $\varepsilon$-optimal with respect to its final prices. This is the explicit operation-count content behind the generic subroutine's analysis in Section 5. It does not claim a bound for a particular data structure or a complete minimum-cost algorithm.

Significance

The theorem gives an order-independent finite bound: the choice of which applicable push or relabel to perform cannot cause generic refine to run forever or stop with an active vertex. Its output is a circulation whose approximate-optimality tolerance has been halved. That output can serve as the next input in the successive-approximation framework. For integral costs, the report's Theorem 2.3 later turns a sufficiently small tolerance into exact minimum cost; that outer-loop result is outside this mission.

This mission specifies the generic cost-scaling state machine in Lean and poses its quantitative analysis as open formalization targets. The shared network and circulation definitions from the published Goldberg–Tarjan 1989 series are available, and a related generic maximum-flow theorem in the 1988 series has a machine-checked proof. Those results do not prove refine's price-based bounds. Contributions that establish the paper's progress, price, or counting statements for this state machine, and reusable facts about finite residual networks, advance the open goal.

Difficulty

A push respects a capacity, but it can create activity at another vertex; a relabel changes which arcs are admissible. Thus checking a single update does not bound an arbitrary sequence. The price bound also depends on the circulation and prices supplied at entry, not merely on the current pseudoflow being $\varepsilon$-optimal. Finally, a vertex with no admissible outgoing arc may appear to be stuck when the relabel minimum is over an empty set. Feasibility of the original circulation network is needed to establish that an active vertex still has a genuine next update. The operation bound requires accounting for the three update types across every possible choice sequence.

Formalization scope

Vertices form a finite type, and capacities, costs, flows, and prices are real-valued functions. The network has symmetric ordered arcs and antisymmetric costs. There is no separate nonnegativity assumption on capacities; feasibility is supplied by the input circulation. The new $\varepsilon$ is positive, so the entry circulation is $2\varepsilon$-optimal before Figure 4 halves the error parameter. The run starts from the resulting saturated pseudoflow and records one applicable push or relabel per index $k<K$. Counts classify those actual steps by the selected arc's residual capacity after a push. Termination is the negation of the paper's loop guard, not a definition that assumes zero excess.

The reduced-cost sign is $c-p(v)+p(w)$, and relabel raises $p(v)$. This differs from the published 1989 epsilon-optimality definition, so only its network model is imported. The relabel relation requires an attained minimum over a nonempty set of outgoing residual arcs; it assigns no default value to an empty minimum. Loops may occur in the reused network model, but cost antisymmetry makes their reduced cost zero, so they cannot be push arcs. The explicit constants are the report's $3n\varepsilon$, $3n(n-1)$, $3nm$, and $3n^2(m+n)$; the goal sums the last three. The report's RAM-model $O(\cdot)$ running times are outside the formal statements. A definition that makes termination equivalent to conservation or assigns an arbitrary relabel price at an empty set would miss the target.

Selected references

• Andrew V. Goldberg and Robert E. Tarjan, Finding Minimum-Cost Circulations by Successive Approximation, MIT/LCS/TM-333, July 1987. Technical report.
• Andrew V. Goldberg and Robert E. Tarjan, Finding Minimum-Cost Circulations by Successive Approximation, Mathematics of Operations Research 15(3), 1990, pp. 430–466. DOI. The report above supplies this mission's numbering.
• Andrew V. Goldberg and Robert E. Tarjan, A New Approach to the Maximum-Flow Problem, Journal of the ACM 35(4), 1988. DOI.
• Andrew V. Goldberg and Robert E. Tarjan, Finding Minimum-Cost Circulations by Canceling Negative Cycles, Journal of the ACM 36(4), 1989. DOI.

Motivation

The diameter of a polyhedron is the largest number of edges needed to travel between two vertices of its graph, its 1-skeleton. Whether this number is bounded by a polynomial in the dimension $d$ and the number of facets $n$ is a long-standing open question in polyhedral combinatorics; edge walks are the moves of vertex-following methods such as the simplex method, so the question bounds what any such method can achieve in the worst case. For fixed dimension, Larman proved in 1970 that the diameter grows at most linearly in $n$, with a constant exponential in $d$ (Larman 1970).

Eisenbrand, Hähnle, Razborov and Rothvoß ask how much of the geometry of polyhedra such upper bounds actually use. They isolate a single combinatorial path property shared by the graphs of non-degenerate polyhedra and announce that the known upper bounds, Larman's among them, "continue to hold in the base abstraction" defined by that property (Dagstuhl abstract, p. 3). The next sentence of the abstract reads: "While the first bound is merely an adaption of the proof in [13], our proof of the second bound is much simpler than the one which was proved for polyhedra in [16]."

The held source is the five-page Dagstuhl extended abstract dated June 15, 2010, which states the results and proves none of them. The full proofs appear in Mathematics of Operations Research 35 (2010), 786–794 (journal article). The goal is an asserted theorem of the paper, not an open conjecture; the formal proof remains to be supplied.

Setting

Let $[n]=\{1,\ldots,n\}$ and write $\binom{[n]}{d}$ for the family of its $d$-element subsets. A graph $G=(V,E)$ in the base abstraction has a nonempty vertex set $V\subseteq\binom{[n]}{d}$: every vertex is a $d$-element set of labels, and distinct vertices carry distinct sets. The edges are arbitrary subject to condition i): for each $u,v\in V$ there exists a path connecting $u$ and $v$ whose intermediate vertices all contain $u\cap v$. Condition i) makes $G$ connected. The class of all such graphs is $\mathcal B_{d,n}$; $d$ is called the dimension and $n$ the number of facets of the abstraction, and $D(d,n)$ denotes the largest diameter of a graph in $\mathcal B_{d,n}$ (p. 2).

The distance $\operatorname{dist}_G(u,v)$ is the least number of edges of a path from $u$ to $v$. The motivating example is the graph of a non-degenerate polyhedron (each vertex on exactly $d$ facets), each vertex labelled by its $d$ facets: two vertices are joined by a path inside the minimal face containing both, and every vertex of that path lies on the facets the two endpoints share (pp. 2–3). The class $\mathcal B_{d,n}$ is not restricted to such graphs.

Formalization targets

Larman's bound in the base abstraction

The abstract prints the bound as $\Delta_u(d,n)\le 2^{d-1}\cdot n$ and states that it continues to hold in the base abstraction. The target is the pointwise form of $D(d,n)\le 2^{d-1}\, n$:

$$\forall d\ge 1,\ \forall n,\ \forall G\in\mathcal B_{d,n},\ \forall u,v\in V(G):\qquad \operatorname{dist}_G(u,v)\le 2^{d-1}\, n .$$

In Lean this is the existence, for every pair $u,v$, of a walk from $u$ to $v$ with at most $2^{d-1}n$ edges. The statement quantifies over every graph satisfying the paper's definition, not over polyhedron graphs or a chosen family.

Significance

For fixed $d$ the bound is linear in $n$, and it holds for a class defined only by finite sets and one path condition. Together with the almost-quadratic lower bound $D(n/4,n)=\Omega(n^2/\log n)$ announced in the same paper, it shows what this one property of polyhedra can and cannot deliver: linear growth in $n$ for fixed dimension, but not a linear bound uniform in $d$ and $n$. Since the graph of every non-degenerate polyhedron lies in $\mathcal B_{d,n}$ (a separate mission of this series), the result also recovers a Larman-type bound for polyhedra, with constant $2^{d-1}$.

Prove2Me already has proved polytope versions: Hirsch.larman_bound (the sharper constant $n\,2^{d-3}$ for nonempty bounded $H$-polytopes), Hirsch.larman_high_dimension, Hirsch.larman_layer_recursion, and Hirsch.tight_row_interval, the polytope form of the interval property that condition i) abstracts. They concern a different object, the vertex-edge graph of an $H$-polytope, and are credited as prior work; none states the bound for every graph of $\mathcal B_{d,n}$. The platform definition Hirsch_clf (connected layer families) is a related abstraction in layered form and is not the graph class used here.

Difficulty

The class contains graphs with no geometric realization, so a proof cannot use convexity, faces as polyhedra, or linear-algebraic facts about vertices; only labels, intersections and walks are available. Condition i) guarantees a path preserving the common labels of two endpoints, but says nothing directly about the length of that path. Mere connectivity on $d$-subsets of $[n]$ gives only the trivial bound $|V|-1\le\binom{n}{d}-1$, which is far from linear in $n$. A linear bound in $n$ has to be extracted from condition i) alone, uniformly over all graphs of the class. The abstract describes its proof only as much simpler than Larman's for polyhedra and states no intermediate lemma, so the mission carries no milestones.

Formalization scope

• $[n]$ is represented by Fin n, labels $0,\ldots,n-1$; only the number of labels matters.
• A vertex set is V : Finset (Finset (Fin n)) and the graph is G : SimpleGraph V; vertices are therefore distinct label sets, as in the paper. InB d n V G requires V.Nonempty, every vertex of cardinality $d$, and CondI V G.
• CondI asks for a walk all of whose vertices contain $u\cap v$. This is the source's path condition: a walk contains a path on a subset of its vertices, and the endpoints contain $u\cap v$ automatically.
• "Continue to hold in the base abstraction" is read as the bound for every graph of $\mathcal B_{d,n}$ and every pair of its vertices. No numeric $D(d,n)$ is defined, so no supremum with a default value enters; a bounded walk witnesses the distance bound.
• $d\ge 1$ is an explicit hypothesis: $d$ is the dimension, and it makes $d-1$ ordinary subtraction in $\mathbb N$. At $d=0$ the class consists only of the one-vertex graph on $\emptyset$, so nothing is lost. For $n<d$ the class is empty.
• The constant is $2^{d-1}$, the paper's constant for the abstraction; the polytope constant $2^{d-3}$ of Hirsch.larman_bound is not claimed here.

Trivializing formalizations are ruled out: labels are the vertices themselves (not an arbitrary labelling that could repeat), and condition i) is required for all pairs, not for one chosen path or only adjacent vertices. A proof only for polyhedron graphs, for graphs with extra structure, or with a larger constant leaves the goal open. Useful contributions include general lemmas about CondI and walk-length bookkeeping for SimpleGraph on a finite vertex type; these are reusable by the other missions of this series.

Selected references

• F. Eisenbrand, N. Hähnle, A. Razborov, T. Rothvoß, Diameter of Polyhedra: Limits of Abstraction, Dagstuhl Seminar Proceedings 10211 (Flexible Network Design), 2010. https://drops.dagstuhl.de/opus/volltexte/2010/2724
• F. Eisenbrand, N. Hähnle, A. Razborov, T. Rothvoß, Diameter of Polyhedra: Limits of Abstraction, Mathematics of Operations Research 35(4), 786–794, 2010. https://doi.org/10.1287/moor.1100.0470
• D. G. Larman, Paths on polytopes, Proceedings of the London Mathematical Society (3) 20, 161–178, 1970. https://doi.org/10.1112/plms/s3-20.1.161

Motivation

The diameter of a polyhedron is the largest number of edges needed to travel between two vertices of its graph. Bounding that number from the dimension and the number of facets is a central question in polyhedral combinatorics because edge walks are the discrete moves available to many vertex-based optimization methods. The Kalai–Kleitman bound gives a quasi-polynomial upper bound in these parameters. Eisenbrand, Hähnle, Razborov and Rothvoß ask how much of the geometry is needed to retain such a bound. They isolate one path property of polyhedron graphs and show that the upper bound persists for every graph satisfying it, including graphs that need not arise from a polyhedron (Dagstuhl abstract, pp. 1–3).

This mission concerns that extension of the Kalai–Kleitman bound. The held source is the five-page Dagstuhl extended abstract dated June 15, 2010. It states the result without its proof. The full proofs appeared in Mathematics of Operations Research 35 (2010), 786–794 (journal article). The goal is an asserted result of the paper, not an open conjecture; the formal proof remains to be supplied.

Setting

Let $[n]=\{1,\ldots,n\}$, and let $\binom{[n]}{d}$ be the family of its $d$-element subsets. A graph $G=(V,E)$ in the paper's base abstraction has a nonempty vertex set $V\subseteq\binom{[n]}{d}$. Thus each graph vertex is labelled by a distinct $d$-element subset. The edges can be chosen freely subject to condition i): for every pair $u,v\in V$, there is a path from $u$ to $v whose intermediate vertices all contain$u\cap v$. The condition implies that the graph is connected. The paper denotes the class of these graphs by$\mathcal B_{d,n}$and calls$d$the dimension and$n$ the number of facets of the abstraction (definition and footnote, p. 2).

The distance between two vertices is the minimum number of edges in a path between them. A graph's diameter is the largest of these distances, and $D(d,n)$ is the largest diameter among graphs in $\mathcal B_{d,n}$. Condition i) is motivated by non-degenerate polyhedra: if a vertex lies on exactly $d$ facets, its tight facets provide a $d$-element label, and two vertices can be connected inside the smallest face containing them. Every vertex on that path retains the facets common to the endpoints (pp. 2–3). This motivation does not restrict $G$ to a realizable polyhedron graph.

Formalization targets

Kalai–Kleitman bound in the base abstraction

For positive dimension, the target is the pointwise form of the paper's assertion that the upper bound continues to hold in the base abstraction:

$$\forall d\geq 1,\ \forall n,\ \forall G\in\mathcal B_{d,n},\ \forall u,v\in V(G),\quad \operatorname{dist}_G(u,v)\leq n^{1+\log_2 d}.$$

Equivalently, every pair has a connecting path with at most $n^{1+\log_2 d}$ edges. Consequently $D(d,n)\leq n^{1+\log_2 d}$. The statement covers every graph with the paper's labels and condition i), rather than a selected realization or a graph with extra geometric properties. The source prints the inequality for $\Delta_u(d,n)$, its polyhedron-diameter notation, and says in the same sentence that it continues to hold for the base abstraction (p. 3).

Significance

The bound shows that a common-facet path property is enough to prevent arbitrarily large diameter once $d$ and $n$ are fixed. It extends an upper bound first attached to graphs of polyhedra to a class specified entirely by finite sets and graph paths. This locates a concrete portion of the polyhedral diameter theory within combinatorics. The same paper gives an almost-quadratic lower bound for the abstraction, so the path property alone does not imply a linear bound in $n$ (p. 3).

A machine-checked proof would connect a precise finite graph model with the real-exponent inequality, without relying on a polyhedron representation. Prove2Me already has a proved theorem called Hirsch.kalai_kleitman_bound for a bounded $H$-polytope, with a different exponent $\log_2 d+2$, and a proved Hirsch.kalai_kleitman_recursion for that polytope model. It also has Hirsch.clf_endpoint_peeling for connected layer families. Those results concern different objects or bounds and are useful prior work, but none is a formalization of the present claim for all $G\in\mathcal B_{d,n}$.

Difficulty

The class permits edges and vertex families with no geometric realization, so a proof cannot use metric or convexity properties of a particular polyhedron. Condition i) guarantees one path preserving the common labels of two endpoints; it does not directly bound that path's length. Connectivity by itself would be too weak: a connected graph on the allowed labels can have a long shortest path unless its labels and the path condition constrain it. The formal task is to obtain the claimed uniform length bound from that condition across all finite families of $d$-sets. The Dagstuhl abstract calls the argument an adaptation of Kalai and Kleitman's proof but states no intermediate lemmas, so this proposal does not assign any in-source milestones (p. 3).

Formalization scope

Lean represents $[n]$ by Fin n, with labels $0,\ldots,n-1$ instead of $1,\ldots,n$; only the number of labels matters. A vertex set is a Finset of Finset (Fin n), and a SimpleGraph has exactly those sets as vertices. This representation enforces distinct labels. InB d n V G requires $V$ to be nonempty, every label to have cardinality $d$, and CondI for every ordered pair. The walk in CondI is equivalent to the source's path: repeated vertices can be erased, and the endpoints themselves contain $u\cap v$. Nonemptiness and condition i) together give the source's connectedness. A path through all graph vertices without the common-intersection condition would be a weaker and inadmissible model.

The theorem takes $d\geq1$, so the logarithm has its ordinary positive-dimension interpretation. The source does not print a logarithm base; the statement reads it as base two, following the cited Kalai–Kleitman convention. This interpretation is explicit in the theorem's prose and is an open source-reading question. The exponent is real: the path length is cast from a natural number to $\mathbb R$ for comparison with $(n:\mathbb R)^{1+\log_2 d}$. No floor is applied to the exponent. The theorem asserts a bounded walk for each pair; that avoids defining $D(d,n)$ through a supremum with an artificial value for an empty class. At $n=0$ with $d\geq1$, InB has no instance, as there are no $d$-element labels; at $d=1$, the bound is $n$, consistent with a connected graph on at most $n$ labels.

The development needs reusable finite-set reasoning about common intersections, graph walks and their lengths, and real-logarithm bounds. Contributions establishing those facts for the paper's CondI model are within scope. A proof only for polyhedron graphs, for graphs with extra edge restrictions, or for a single chosen graph would leave the goal open.

Selected references

• F. Eisenbrand, N. Hähnle, A. Razborov and T. Rothvoß, Diameter of Polyhedra: Limits of Abstraction, Dagstuhl Seminar Proceedings 10211, 2010. Extended abstract.
• F. Eisenbrand, N. Hähnle, A. Razborov and T. Rothvoß, Diameter of Polyhedra: Limits of Abstraction, Mathematics of Operations Research 35, 786–794, 2010. DOI.

Motivation

Finding the quickest route between two points of a road network is among the oldest problems of operations research. It is the subproblem inside vehicle routing, network flow and many dynamic programs. Richard Bellman's four-page note On a routing problem (Quarterly of Applied Mathematics, 1958) treats it as a dynamic program. The minimal travel times satisfy a nonlinear system of equations, and that system can be solved by successive approximations that terminate after a number of steps bounded in advance. The iteration is now known as the Bellman–Ford method. A footnote added in proof records that Max Woodbury and George Dantzig had obtained the same scheme independently, and Ford's RAND report of 1956 describes a closely related labelling procedure.

Timeline.

• 1956. L. R. Ford Jr., Network flow theory (RAND P-923): a label-improving procedure for shortest paths.
• 1957. Bellman's Dynamic Programming (Princeton) states the principle of optimality used here.
• 1958. Bellman's note: the routing equation, its uniqueness, approximation in policy space with an (N − 1)-step bound, and a second, monotone increasing scheme.
• 1959. Dijkstra gives a label-setting method for nonnegative lengths.
• 1962. Floyd's Algorithm 97 computes all pairs of shortest distances.

Setting

There are $N$ cities, numbered $1, \dots, N$. Every two of them are linked by a direct road, and city $N$ is the destination. The travel time from $i$ to $j$ is a real number $t_{ij}$; the matrix $T = (t_{ij})$ need not be symmetric. Throughout, $t_{ij} > 0$ for $i \ne j$.

A route from $i$ to $N$ is a sequence of cities $i = c_0, c_1, \dots, c_m = N$ in which consecutive cities differ. Its stops are $c_1, \dots, c_{m-1}$, and its time is $\sum_{r<m} t_{c_r c_{r+1}}$. The minimal time $f_i$ (3.1) is the least time of a route from $i$ to $N$, and $f_N = 0$.

The routing equation (3.2) is the system

$$F_i = \min_{j \ne i}\,[t_{ij} + F_j]\quad (i = 1, \dots, N-1), \qquad F_N = 0 .$$

Approximation in policy space (§5) starts from the direct-route policy (5.2), $f_i^{(0)} = t_{iN}$, and iterates (5.1):

$$f_i^{(k+1)} = \min_{j \ne i}\,[t_{ij} + f_j^{(k)}]\quad (i \ne N), \qquad f_N^{(k+1)} = 0 .$$

The second scheme (§7, (7.1)) starts instead from $\underline f_i^{(0)} = \min_{j\ne i} t_{ij}$ and uses the same step.

Formalization targets

Goal: convergence within $N - 1$ iterations

For every $k \ge N - 1$ the following hold. Each $f_i^{(k)}$ is the minimal time from $i$ to $N$, attained by a route. The vector $f^{(k)}$ solves (3.2). Every real solution of (3.2) equals $f^{(k)}$:

$$k \ge N-1 \;\Longrightarrow\; f^{(k)} = f = \text{the unique solution of (3.2)}.$$

This is the claim of the Summary ("converges after at most $(N-1)$ iterations") and of the last sentence of §5. The paper's bound $N - 1$ is kept, although $N - 2$ also suffices.

Milestones

1. (3.2): the minimal times exist and satisfy the routing equation.
2. §4: (3.2) has at most one solution.
3. (5.4): $f^{(1)} \le f^{(0)}$.
4. §5, the sentence after (5.4): $f_i^{(k)}$ is the minimal time over routes with at most $k$ stops.
5. (5.5): $f^{(k+1)} \le f^{(k)}$ for all $k$.
6. §7: the scheme (7.1) increases, stays below the solution of (3.2) (7.2), and equals it from some index on.

Significance

The result. The note turns an enumeration over exponentially many paths into $N - 1$ rounds of $N$ minimisations each, with a bound fixed before the computation starts. The uniqueness theorem makes the routing equation a characterisation of the minimal times, not merely a property of them. This is the template for later correctness proofs of shortest-path and value-iteration algorithms. The monotone decrease (5.5) is the first instance of policy improvement: every iterate is the value of an actual routing policy.

Formalizing it. The results are classical and proved. What this mission adds is a machine-checked development against the paper's own objects. Routes, their times and minimal times are defined from scratch. The iteration is stated exactly as printed, apart from the corrected initial value at the destination. The (N − 1)-step termination is asserted as an equality, not a limit. Related platform items treat other methods and do not cover these statements. One is the label-correcting method (BertsekasDP.label_correcting_correctness_of_nonneg_arcs, BertsekasDP.label_correcting_terminates). Another is the stochastic shortest path problem under a termination assumption that fails for deterministic routing (BertsekasDP.ssp_main_theorem). There are also the generic candidate-list algorithm (BertsekasNetwork.generic_shortest_path_algorithm), Floyd's Algorithm 97 and Dijkstra's method.

Difficulty

The minimum in (3.2) may be attained at a $j$ whose own optimal route passes back through $i$. The routing equation is a fixed-point equation for an operator that is monotone but not a contraction in any fixed norm. The standard contraction argument for discounted dynamic programs therefore does not apply. Uniqueness has to use $t_{ij} > 0$ to exclude zero-time cycles: with $t_{12} = t_{21} = 0$, the system (3.2) has infinitely many solutions. The $N - 1$ bound depends on the at-most-$k$-stops reading of $f^{(k)}$ and on the fact that an optimal route never needs to revisit a city. Neither is visible from the recursion alone. For the scheme of §7, the page gives no bound on the number of iterations, and none holds uniformly in $t$.

Formalization scope

Cities are Fin (n + 1), so $N = n + 1$, with standing hypothesis $n \ge 1$. City $N$ is Fin.last n, and travel times are t : Fin (n + 1) → Fin (n + 1) → ℝ with $t_{ij} > 0$ for $i \ne j$. Diagonal entries are unconstrained and never used. No symmetry, triangle inequality or integrality is assumed. A route is a list of cities with distinct consecutive entries ending at $N$. Repeated cities are allowed; with positive times this changes no minimum. Minimal times are attained minima over routes (IsMinTime, IsMinTimeWithin), not real infima. The minimum in (3.2) is a Finset.inf' over all $j \ne i$, the destination included.

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

• "Using an optimal policy" (3.1) becomes a minimum attained by a route and below every route.
• "Represents the minimum time for a path with at most one stop" becomes, for every $k$, a minimum over routes with at most $k + 1$ roads.
• "Converges after at most $(N - 1)$ iterations" becomes $f^{(k)} = f$ for every $k \ge N - 1$.
• "Only a finite number of iterations will be required" (§7) becomes $\exists K, \forall k \ge K$, $\underline f^{(k)} = f$.
• "The solution of (3.2)" in §7 becomes an arbitrary solution of (3.2), which milestones 1–2 show is the vector of minimal times.

Two printed slips are corrected. (5.2) is printed for $i = 1, \dots, N$, which would set $f_N^{(0)} = t_{NN}$, and with $t_{NN} > 0$ statements (5.4), (5.5) and the goal would be false. The formalization uses $f_N^{(0)} = 0$, the value the paper's own justification needs. (7.1) prints "$N = 1$" for $N - 1$. Section 6 (computational aspects) and the closing expectation of §7 that the first method converges faster are not formalized.

The goal cannot be satisfied trivially. The minimal times are defined from routes, not as a solution of (3.2) or as a limit of the iteration, so the goal connects the recursion to the routing problem itself.

The development needs only finite minima, lists and induction; nothing beyond core Mathlib. The route and minimal-time layer is reusable for other deterministic shortest-path results. Proofs of any milestone are welcome, as are proofs of the sharper bound $N - 2$.

Selected references

• R. Bellman, On a routing problem, Quarterly of Applied Mathematics 16(1) (1958), 87–90. https://doi.org/10.1090/qam/102435
• R. Bellman, Dynamic Programming, Princeton University Press, 1957.
• R. Bellman, The theory of dynamic programming, Bull. Amer. Math. Soc. 60 (1954), 503–515. https://doi.org/10.1090/S0002-9904-1954-09848-8
• L. R. Ford Jr., Network flow theory, RAND Corporation P-923, 1956. https://www.rand.org/pubs/papers/P923.html
• E. W. Dijkstra, A note on two problems in connexion with graphs, Numerische Mathematik 1 (1959), 269–271. https://doi.org/10.1007/BF01386390
• R. W. Floyd, Algorithm 97: Shortest path, Communications of the ACM 5(6) (1962), 345. https://doi.org/10.1145/367766.368168