Combinatorics

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:

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

Large zero–one linear programs can contain constraints involving only a small fraction of their variables. Crowder, Johnson and Padberg study how to extract useful inequalities from one such row while solving the larger program. Their computational method identifies a violated inequality at a current linear programming solution, adds it, and resolves the relaxation. The mathematical question behind that step is whether a minimal cover inequality can be found by a separate optimization problem. The authors answer it in Section 2.3 of their 1983 paper, after developing cover and configuration inequalities in Section 2.2. Crowder, Johnson and Padberg (1983)

The target is a known result from that paper. It is a precise statement about a finite knapsack row and a point in the unit cube, independent of the paper's implementation and numerical experiments. The paper also discusses $(1,k)$-configurations and lifting, which turn the identified inequalities into valid cuts involving additional row variables. Those statements supply the mission's milestones and make the separation result useful in its original setting. Crowder, Johnson and Padberg (1983), Sections 2.2–2.4

Setting

Fix a finite index set $K$, positive rational coefficients $a_j$ for $j\in K$, and a rational right-hand side $a_0$. A zero–one solution is a vector with each $x_j\in\{0,1\}$ satisfying the single row

The model uses the support set $x=\{j:x_j=1\}$ for such a vector. A set $S\subseteq K$ is a minimal cover when its total coefficient exceeds $a_0$, but removing any one member makes the total at most $a_0$:

It yields the cover inequality $\sum_{j\in S}x_j\le |S|-1$ for every feasible zero–one vector. The right-hand side is interpreted as a real number, so the expression also has its usual meaning when $S$ is empty.

A $(1,k)$-configuration consists of $S^*\subseteq K$, $t\notin S^*$ and an integer $2\le k\le |S^*|$. The set $S^*$ itself fits the row, while $Q\cup\{t\}$ is a minimal cover for every $k$-element subset $Q$ of $S^*$. For any $k\le r\le |S^*|$ and $r$-element $T\subseteq S^*$, its inequality is $(r-k+1)x_t+\sum_{j\in T}x_j\le r$. Crowder, Johnson and Padberg (1983), pp. 810–811

For a point $\bar x\in[0,1]^K$, the separation problem asks for a cover $s\subseteq K$ minimizing $\sum_{j\in s}(1-\bar x_j)$, subject to the strict condition $\sum_{j\in s}a_j>a_0$. This is problem (2.12). The set of attainable values is finite, but it is empty if the row has no cover. An optimal value $z$ is therefore asserted only when a least attainable value exists.

Formalization targets

Cover separation

The goal is the paper's Section 2.3 equivalence:

where $z$ is the attained optimum of (2.12). A cover inequality cuts off $\bar x$ precisely when its left-hand side exceeds $|S|-1$. If there is no cover, (2.12) has no optimal value; the theorem does not assign it an artificial value. Crowder, Johnson and Padberg (1983), pp. 812–813

Valid inequalities and lifting

The milestones state the validity of (2.7) and every inequality in (2.9), the two assertions used in the separation equivalence, and the relaxed lifting claims of Section 2.4. For lifting, $z_k$ is the maximum integer objective value in (2.10), $\bar z_k$ is the maximum in its linear relaxation, and $z_k^*=\lfloor\bar z_k\rfloor$. The claims are $z_k\le z_k^*$ and validity after adding variable $k$ with coefficient $f_k=f_0-z_k^*$. They concern attained optima, as the paper's “maximum” language requires. Crowder, Johnson and Padberg (1983), pp. 811, 814

Significance

The equivalence turns a geometric question about which cover inequality excludes $\bar x$ into a finite optimization test with a numerical threshold of one. It identifies when a minimal cover cut exists for a row, while the validity milestones certify that the inequalities can be added without removing zero–one feasible points. The lifting claims explain how an inequality first written on a subset of variables remains valid as further variables enter it. These are the mathematical guarantees used by the paper's cutting plane procedure. Crowder, Johnson and Padberg (1983), Sections 2.2–2.4

The paper proves the separation equivalence and states the surrounding validity claims. This mission records their exact statements in Lean; its theorem proofs remain open. A complete development would add machine-checked proofs for the finite cover argument, configuration inequalities, and lifting validity. The resulting definitions of feasible supports, attained optimization values and intermediate inequality validity can also be reused in other finite knapsack formalizations.

Difficulty

Checking all subsets of $K$ directly grows rapidly with the row size. A separation result must relate a minimum over all covers to an inequality indexed by a minimal cover, while accounting for objective coefficients that may be zero when $\bar x_j=1$. The same boundary matters for lifting: the zero–one maximum is compared with a continuous relaxation, and rounding is justified by the integer coefficients of the current inequality. If the lifting problem is infeasible, neither maximum exists. Crowder, Johnson and Padberg (1983), pp. 812–814

Formalization scope

Lean uses an arbitrary finite index type for $K$, replacing the paper's indices $1,\ldots,n$. A zero–one vector is a finite support set. Row coefficients and $a_0$ are rational, as on p. 810; the point $\bar x$ and separation values are real. The target asks only that $\bar x$ lie in the unit cube. Although the paper obtains it as an optimum of the full LP relaxation (2.11), that additional property is not used in the row-level equivalence. No sign condition is imposed on $a_0$.

The strict knapsack condition in (2.12) is retained. “Chops off” means strict violation of (2.7). “Optimal value” means membership and leastness in the attainable value set; for lifting it means membership and greatestness. Thus rows with no cover or infeasible lifting subproblem do not acquire a default zero optimum. The size expressions $|S|-1$ and $r-k+1$ are evaluated in the reals, so natural-number truncation cannot change them. Integer lifting coefficients and the floor of the relaxed optimum express the paper's “truncating to its integer part”; the feasible relaxed problem includes the zero vector, so this agrees with truncation toward zero there.

Validity during an intermediate lifting step ranges over feasible zero–one vectors supported in the current set $S$. After adding $k$, it ranges over support in $S\cup\{k\}$. The final inequality covers the whole row when that set is $K$. The development must preserve the full quantifier over every $k$-subset in (2.8) and every $r$ and $T$ in (2.9); restricting these would weaken the paper's claim. Contributions proving the named milestones, adding concrete examples, or developing general finite optimization lemmas are in scope. The facet assertions attributed to Padberg are outside the target. A related lifted-cover facet statement already appears on the platform as NemhauserWolsey.partitioned_cover_lifting_defines_facet; its conventions and claim differ from this mission's validity results.

Selected references

• H. Crowder, E. L. Johnson and M. Padberg, Solving Large-Scale Zero-One Linear Programming Problems, Operations Research 31(5), 803–834, 1983. DOI: 10.1287/opre.31.5.803

Motivation

The single-machine scheduling problem $1|\mathrm{prec}|\sum w_j C_j$ asks for an order in which to process $n$ jobs, each with a processing time and a weight, on one machine, respecting a partial order of precedence constraints, so that the weighted sum of completion times is as small as possible. It is NP-hard, and the best known approximation ratio for general precedence constraints is $2$. Ambühl, Mastrolilli, Mutsanas and Svensson (Math. Oper. Res. 36(4), 2011) relate the problem to the dimension theory of partial orders: their Theorem 3.2 states that when the precedence constraints are given together with a realizer of size $k$, the problem has a $(2 - 2/k)$-approximation algorithm. Small realizers of structured precedence orders therefore translate directly into better approximation ratios.

This mission formalizes one such structural result, Lemma 4.1 of the paper: every convex bipartite order has a realizer of size $3$. Convex bipartite orders form a class of precedence constraints that lies strictly between strong bipartite orders and general bipartite orders (Möhring, 1989). Combined with Theorem 3.2, the lemma gives a $4/3$-approximation for $1|\mathrm{prec}|\sum w_j C_j$ on this class. According to the authors, the bound $\dim \le 3$ for convex bipartite orders had not been known before.

Setting

A poset is a set $N$ with a reflexive, antisymmetric, transitive relation $P$. Two elements $x, y$ are incomparable, written $x \parallel y$, when neither $(x,y) \in P$ nor $(y,x) \in P$; the set of incomparable pairs is $\mathrm{inc}(P)$. A linear extension of $P$ is a linear order $L$ on $N$ with $P \subseteq L$. A linear order $L$ reverses the pair $(x,y)$ when $y < x$ in $L$. A realizer of size $t$ is a family $L_1, \dots, L_t$ of linear extensions of $P$ such that every incomparable pair $(x,y)$ is reversed by at least one $L_i$. The dimension $\dim(P)$ is the least $t$ for which a realizer of size $t$ exists.

A convex bipartite order has jobs $N = J^- \cup J^+$ split into minus jobs $J^- = \{j_1, \dots, j_a\}$ and plus jobs $J^+ = \{j_{a+1}, \dots, j_n\}$. Each plus job $j_k$ carries two indices $1 \le l(k) \le r(k) \le a$, and a minus job $j_i$ precedes $j_k$ exactly when $l(k) \le i \le r(k)$. There are no other precedences: the predecessors of each plus job form a nonempty interval of consecutive minus jobs.

For the Appendix construction, the incomparable pairs are sorted into three sets $E_1, E_2, E_3$ according to the kinds of the two jobs, the order of their indices and, for a pair (plus job $j_i$, minus job $j_j$), whether $j_j$ precedes some plus job of larger index than $i$. The sets $\bar E_m = E_m \cup P$ describe what the $m$-th linear order of the realizer must contain.

Formalization targets

Goal: Lemma 4.1

Equivalently, $\dim(P) \le 3$. The goal holds for every numbering of the jobs and every choice of interval ends $l, r$.

Milestones

• Lemma A.1. $E_1, E_2, E_3$ partition $\mathrm{inc}(P)$, and for each $m$, $(x,y) \in E_m$ implies $(y,x) \notin E_m$.
• Lemma A.2. Under the Appendix's numbering of the plus jobs ($i < j$ implies $l(i) \le l(j)$), each $\bar E_m$ is contained in a linear order on $N$.

Significance

The result. Lemma 4.1 places convex bipartite orders among the classes of precedence constraints for which $1|\mathrm{prec}|\sum w_j C_j$ has an approximation ratio strictly below $2$, namely $4/3$ through Theorem 3.2 of the paper. The bound is tight: a bipartite order has dimension $2$ exactly when it is a strong bipartite order (Möhring), so the bound $3$ cannot be lowered for the class of convex bipartite orders. Since $\dim(P) = 3$ also gives $\chi(G_P) = 3$ for the graph of incomparable pairs, a $3$-realizer yields an optimal colouring of that graph.

Formalizing it. The result is proved in the paper, with a short case analysis in the Appendix. No machine-checked proof is known to exist. Mathlib has no dimension theory of posets: realizers, reversals of incomparable pairs and the construction of linear extensions containing a given acyclic relation have to be set up here. The definitions of realizer and linear extension are stated for an arbitrary relation and can be reused for other dimension bounds (interval orders, semiorders, the other missions of this series).

Difficulty

The three relations $\bar E_m$ are not partial orders. $\bar E_2$, for instance, is not transitive: with two minus jobs and one plus job $j_3$ with $l(3) = r(3) = 2$, the pairs $(j_1, j_2) \in E_2$ and $(j_2, j_3) \in P$ are present but $(j_1, j_3)$ lies in $E_1$. The step that requires work is to show that each $\bar E_m$ has no cycle, so that it extends to a linear order. For $\bar E_2$ this depends on the convexity of the predecessor intervals and on the numbering of the plus jobs by their left ends: it is not a consequence of bipartiteness alone. The goal itself carries no numbering assumption, so any proof must also account for renumbering the plus jobs.

Formalization scope

All declarations live in the namespace SingleMachinePrec.ConvexBipartite.

• Relations. A relation on $N$ is a predicate N → N → Prop. Linear orders use Mathlib's unbundled class IsLinearOrder. A linear extension of $P$ is a linear order $L$ with $P \subseteq L$; $L$ reverses $(x,y)$ when $L\,y\,x$ and $y \ne x$. A realizer of size $t$ is a function Fin t → N → N → Prop, so repeated members are allowed, as in the paper's multisets.
• Convex bipartite orders. The jobs are the type Fin a ⊕ Fin b: Sum.inl i is the minus job $j_{i+1}$, Sum.inr k the plus job $j_{a+k+1}$, with indices starting at $0$. The interval ends are maps l r : Fin b → Fin a with l k ≤ r k, and $P$ is equality together with the pairs (minus $i$, plus $k$) with $l(k) \le i \le r(k)$. A file-level instance records that $P$ is a partial order. Any convex bipartite order in the paper's sense is one of these after naming its jobs. The cases $a = 0$ and $b = 0$ are allowed.
• $E_1, E_2, E_3$. Each set is defined as "incomparable and satisfies the paper's case condition". In the plus–minus clauses, "$k > i$" compares plus indices, because $k$ exceeds the index of a plus job.
• Lemma A.2. "$\bar E_m$ is an extension of $P$" is formalized as "there is a linear order containing $\bar E_m$", which is what the paper's proof establishes (absence of cycles) and what its final paragraph uses. Reading it as "$\bar E_m$ is a partial order" would make the lemma false (see Difficulty). The Appendix's numbering assumption is the hypothesis Monotone l of this milestone only.
• Algorithmic wording not formalized. The paper states Lemma 4.1 as "a realizer of size 3 can be computed in polynomial time". What is formalized is the existence of the realizer; the running time is not.

A trivializing formalization would let the members of the realizer be arbitrary relations, which makes reversing every pair free. Here every member must be a linear order containing $P$.

Contributions welcome: proofs of the two milestones and of the goal; a general lemma that a relation whose transitive closure is antisymmetric extends to a linear order on a finite type; and the renumbering argument that removes the numbering assumption.

Selected references

• C. Ambühl, M. Mastrolilli, N. Mutsanas, O. Svensson, On the Approximability of Single-Machine Scheduling with Precedence Constraints, Mathematics of Operations Research 36(4):653–669, 2011. https://doi.org/10.1287/moor.1110.0512
• G. R. Brightwell, E. R. Scheinerman, Fractional dimension of partial orders, Order 9(2):139–158, 1992.
• R. H. Möhring, Computationally tractable classes of ordered sets, in I. Rival (ed.), Algorithms and Order, NATO ASI Series 255, Kluwer, 1989, pp. 105–193.
• W. T. Trotter, Combinatorics and Partially Ordered Sets: Dimension Theory, Johns Hopkins University Press, 1992.

Motivation

Vertex connectivity measures how robust a network is against the failure of nodes. It can be measured in two ways that look different. One way counts the fewest nodes whose removal disconnects the network. The other counts the routes between two nodes that share no intermediate node. Whitney's theorem (1932) says that the two measures agree for every pair of nodes. It is the vertex form of Menger's theorem, and it underlies reliability analysis of communication and transportation networks, the design of fault-tolerant routing, and much of structural graph theory.

M. L. Balinski's 1961 paper On the graph structure of convex polyhedra in n-space proves that the graph of a bounded full-dimensional polyhedron in $n$-space is $n$-tuply connected (the subject of Mission I of this series). It then invokes Whitney's theorem to conclude that any two vertices of such a polyhedron are joined by $n$ disjoint paths. Balinski gives a short new proof of Whitney's theorem through the max-flow min-cut theorem of Ford and Fulkerson and of Dantzig and Fulkerson. That makes the theorem a consequence of linear programming duality. This mission formalizes that part of the paper: the network vocabulary, the max-flow min-cut theorem with capacities on both points and lines, the integrality of maximum flows, and Whitney's theorem itself.

Timeline.

• 1927: Menger states the disjoint-paths theorem for separating sets.
• 1932: Whitney proves the characterization of $n$-connected graphs by $n$ disjoint paths between every pair of points.
• 1956: Ford and Fulkerson and Dantzig and Fulkerson prove the max-flow min-cut theorem.
• 1961: Balinski derives Whitney's theorem from it with a unit-capacity network.

Setting

A graph $G$ consists of a finite set $V$ of points and a set of lines, each line being a pair of distinct points. A path from $p_s$ to $p_k$ is a sequence of lines $(p_1,p_2),(p_2,p_3),\dots,(p_m,p_{m+1})$ with $p_1 = p_s$, $p_{m+1} = p_k$ and $m \ge 1$. Paths are disjoint if they have no point in common except possibly their first and last points.

$G$ is $n$-tuply connected if it has at least $n+1$ points and, for every set $X$ of fewer than $n$ points, the graph $G - X$ remaining after deleting $X$ is connected. $G$ has $n$ disjoint paths from $p_s$ to $p_k$ if there are $n$ pairwise distinct paths from $p_s$ to $p_k$, none of which repeats a point, and no two of which share a point other than $p_s$ and $p_k$.

A network is a connected graph with a capacity $c(x) \ge 0$ on every point and $c(e) \ge 0$ on every line, and with a distinguished source $p_s$ and sink $p_k$. A flow assigns a number $f(C) \ge 0$ to every path $C$ from $p_s$ to $p_k$, such that for every point $x$ and every line $e$

Its value is $\operatorname{val}(f) = \sum_C f(C)$. A disconnecting set is a pair $(X,F)$ of points and lines that meets every walk from $p_s$ to $p_k$. Its value is $\sum_{x\in X} c(x) + \sum_{e \in F} c(e)$.

The unit network of the proof has capacity $1$ on every point except $p_s$ and $p_k$, and capacity $n+1$ on every line except the line $p_sp_k$ (if present), which has capacity $1$. In Lean these are IsNTuplyConnected, HasNDisjointPaths, IsFlow, flowValue, IsDisconnecting, cutValue, unitCapV and unitCapE, all in the namespace Balinski61.Whitney.

Formalization targets

Goal: Whitney's theorem (p. 434)

For a finite graph $G$ with at least two points and any $n \ge 0$:

Both directions are part of the goal.

Milestones, in the order of the proof

1. Max-flow min-cut (p. 433). In every network there is a number $M$ that is the value of some flow and of some disconnecting set, with every flow of value at most $M$ and every disconnecting set of value at least $M$.
2. Integrality (p. 434). If all capacities are integers, some maximum flow has only integer path flows.
3. Min-cut in the unit network (p. 434). If $G$ is $n$-tuply connected and $p_s \ne p_k$, every disconnecting set of the unit network has value at least $n$.
4. Paths from unit flows (p. 434). An integral flow of value at least $n$ in the unit network yields $n$ disjoint paths from $p_s$ to $p_k$.
5. Sufficiency (p. 434). If every pair of distinct points is joined by $n$ disjoint paths, $G$ is $n$-tuply connected.

Significance

Whitney's theorem turns a statement about all small deletion sets into the existence of explicit, verifiable path systems, and back again. In applications it certifies connectivity by exhibiting paths, and it certifies that connectivity is no larger by exhibiting a separating set. It is the base of the theory of $k$-connected graphs: ear decompositions, the fan lemma, and the structure of minimally $k$-connected graphs all use it. Inside this paper it supplies the COROLLARY that any two vertices of a bounded full-dimensional polyhedron in $n$-space are joined by $n$ disjoint edge paths.

None of these results is formalized for vertex connectivity at this Mathlib revision. Mathlib has edge connectivity and connected components but no vertex Menger theorem. The Prove2Me library has max-flow min-cut statements for arc capacities only and integrality results for basic solutions of network LPs, but no flow model with capacities on points. A completed development gives a reusable vertex-capacitated max-flow min-cut theorem for undirected graphs and the first machine-checked Whitney theorem in this library. The results are classical and proved; the remaining work is the formalization.

Difficulty

The sufficiency direction is elementary. The necessity direction needs a global object (a flow, or a family of paths) to exist from purely local hypotheses about deletions. The obvious induction on $n$, which deletes a point and applies the hypothesis to a smaller graph, does not keep the path systems disjoint. In Balinski's route the weight falls on max-flow min-cut and integrality for path flows with capacities on points, neither of which exists in the library. A second difficulty sits in a case the paper's proof skips: a disconnecting set of the unit network may use the line $p_sp_k$ (capacity $1$) together with up to $n-2$ points, and the deletion hypothesis of $n$-tuple connectedness speaks only about points.

Formalization scope

Graphs are Mathlib SimpleGraphs on a Fintype with decidable equality and adjacency. Paths are walks with IsPath. A flow is a real function on the finite type G.Path ps pk of simple paths; "through a point" and "through a line" mean membership in the walk's support and edge list. Capacities are functions V → ℝ and Sym2 V → ℝ. Nonnegativity, connectivity of $G$ and $p_s \ne p_k$ are hypotheses of the network theorems.

The following readings of loose phrases are explicit in the statements:

• "dropping out $n-1$ or fewer points" is $|X| < n$;
• "$n$ disjoint paths" means $n$ pairwise distinct simple paths. The printed path syntax permits repeated vertices; in a graph with lines $p_s a$, $p_s b$, and $p_s p_k$, the distinct walks $p_s,a,p_s,p_k$ and $p_s,b,p_s,p_k$ share only their endpoints even though the graph is not $2$-tuply connected. The theorem therefore uses its conventional simple-path reading;
• path flows live on simple paths (merging and shortcutting changes no maximum value);
• the paper leaves the capacities of $p_s$ and $p_k$ in the unit network unassigned, and here they are $n+1$;
• "the condition is sufficient is obvious" is the full statement that $n$-tuple connectedness follows;
• the hypothesis $|V| \ge 2$ is added to the goal and to sufficiency, because the paper's "any pair of points" presupposes it and the equivalence fails for a one-point graph.

The max-flow min-cut milestone states that the maximum and the minimum are attained. A statement that only bounds some flow by every cut is satisfied by the zero flow. A connectivity notion without the $n+1$ point count would make every complete graph $n$-connected for all $n$. Both trivializations are excluded.

Contributions welcome: a vertex-capacitated augmenting-path or LP-duality proof of max-flow min-cut for path flows, integrality by an augmenting-path argument, the unit-network lemmas, and direct combinatorial proofs of Whitney's theorem that bypass flows.

Selected references

• M. L. Balinski, On the graph structure of convex polyhedra in n-space, Pacific J. Math. 11 (1961), 431–434. https://doi.org/10.2140/pjm.1961.11.431
• H. Whitney, Congruent graphs and the connectivity of graphs, Amer. J. Math. 54 (1932), 150–168. https://doi.org/10.2307/2371086
• L. R. Ford, Jr. and D. R. Fulkerson, Maximal flow through a network, Canadian J. Math. 8 (1956), 399–404. https://doi.org/10.4153/CJM-1956-045-5
• G. B. Dantzig and D. R. Fulkerson, On the max-flow min-cut theorem of networks, in Linear Inequalities and Related Systems, Ann. of Math. Stud. 38, Princeton Univ. Press, 1956, 215–221. https://doi.org/10.1515/9781400881987
• K. Menger, Zur allgemeinen Kurventheorie, Fund. Math. 10 (1927), 96–115. https://doi.org/10.4064/fm-10-1-96-115

Motivation

The problem $1\,|\,\mathrm{prec}\,|\,\sum w_jC_j$ asks for a single-machine sequence of jobs, respecting precedence constraints, that minimizes the weighted sum of completion times. It has been known to be strongly NP-hard since Lawler (1978) and Lenstra and Rinnooy Kan (1978), several different 2-approximation algorithms are known, and closing the approximability gap is listed by Schuurman and Woeginger (1999) as one of ten outstanding open problems in scheduling theory. Ambühl, Mastrolilli, Mutsanas and Svensson (Math. Oper. Res. 36(4), 2011) give the first inapproximability result for this problem: under a widely believed complexity assumption it has no polynomial-time approximation scheme (PTAS). The bridge to that result is a quantitative link, Lemma 9.1, between the optimal value of a special bipartite scheduling instance and the maximum edge biclique of a bipartite graph, a problem whose hardness of approximation was established by Ambühl, Mastrolilli and Svensson (FOCS 2007). This mission formalizes that link.

Setting

A schedule of a finite job set is a sequence $\sigma$ listing every job once; the machine processes the jobs in that order from time $0$ without idle time or pre-emption. Job $j$ has a processing time $p_j$ and a weight $w_j$; its completion time $C_j$ is the sum of the processing times of the jobs up to and including $j$, and the value of $\sigma$ is $\mathrm{val}(\sigma)=\sum_j w_jC_j$. Precedence constraints are a relation $P$ on jobs: $(i,j)\in P$ with $i\ne j$ means job $i$ must be completed before job $j$ starts. A schedule respecting all of them is feasible, and a feasible schedule $\sigma^*$ of least value is optimal.

Let $G=(U,V,E)$ be an $n$-by-$n$ bipartite graph: $|U|=|V|=n$ and $E\subseteq U\times V$. An edge biclique is a pair $A\subseteq U$, $B\subseteq V$ with $A\times B\subseteq E$, of value $|A|\cdot|B|$; the maximum edge biclique problem (Definition 9.1) asks for one of largest value. The bipartite scheduling instance $S_G$ has jobs $U\cup V$ and precedence constraints

so $u\in U$ must precede $v\in V$ exactly when $(u,v)$ is not an edge. Jobs of $U$ have $p=1$, $w=0$; jobs of $V$ have $p=0$, $w=1$. Thus $\mathrm{val}(\sigma)=\sum_{v\in V}C_v$, where $C_v$ is the number of $U$-jobs scheduled before $v$. For $i\ge1$, $\sigma(i)$ denotes the number of $V$-jobs scheduled before $i$ jobs of $U$ have been scheduled.

In the Lean development these are weightedCompletion, IsOptimalSchedule, IsEdgeBiclique, maxBicliqueValue, precSG, procSG, weightSG, valSG, IsOptimalSG and vBefore in the namespace SingleMachinePrec.Biclique.

Formalization targets

Goal: Lemma 9.1 (p. 666)

If a maximum edge biclique of $G$ has value $an^2$ with $a\in(0,1]$, then $S_G$ has an optimal schedule and every optimal schedule $\sigma^*$ satisfies

Milestones (proof of Lemma 9.1, §9, p. 666)

1. For every edge biclique $(A,B)$, a schedule in the block order $U\setminus A\to B\to A\to V\setminus B$ exists, and every such schedule is feasible with

2. For every schedule, $\sigma(n+1)=n$ and

3. For every feasible schedule and $i=1,\dots,n$,

Significance

Lemma 9.1 shows that the optimal value of $S_G$ determines the maximum edge biclique of $G$ up to a factor of order $\ln(1/a)$ in the "area above the work line" $n^2-\mathrm{val}(\sigma^*)$. Combined with the hardness of approximating maximum edge biclique (Theorem 9.1, cited from Ambühl, Mastrolilli and Svensson 2007) it yields Theorem 9.2: $1\,|\,\mathrm{prec}\,|\,\sum w_jC_j$ has no PTAS unless SAT can be decided by a probabilistic algorithm in time $2^{N^\epsilon}$ for every $\epsilon>0$. It also makes precise the two-dimensional Gantt chart picture of Eastman, Even and Isaacs (1964) and of Goemans and Williamson (2000), in which every point on the work line of a schedule defines an edge biclique.

The lemma is proved in the paper; it is not formalized anywhere to our knowledge. A formal proof certifies the combinatorial core of the no-PTAS result independently of the complexity-theoretic layer, and its definitions (the bipartite instance $S_G$, edge bicliques, the profile $\sigma(i)$) are reusable for the gap inequality behind Theorem 9.2.

Difficulty

The upper bound is a direct computation on one explicit schedule. The lower bound is a statement about every feasible schedule, of which there are exponentially many, and it must hold with the explicit constant $2$ and the factor $\ln(1/a)$ for every $a\in(0,1]$. The printed argument splits the sum at $i=(1-a)n$ and uses $\lfloor an\rfloor$, treating $an$ as an integer; for general $a$ (for example $n=3$, value $2$, $an=2/3$) the split point is not an integer, so the printed estimate does not apply verbatim and the constant $2$ has to be re-checked for non-integral $an$. On the formal side, the value identity requires relating completion times in a list to counting $U$-jobs before each $V$-job, with ties among zero-length jobs.

Formalization scope

Jobs are the disjoint union U ⊕ V of two finite types with Fintype.card U = Fintype.card V = n; $E$ is a relation U → V → Prop. A schedule is a duplicate-free list containing every job; feasibility is the published LawlerPrec.MinMax.IsFeasible and completion times are the published MooreLateJobs.Shared.completionTime (time $0$ start, no idle time). Processing times and weights are reals, here in $\{0,1\}$. The maximum edge biclique value is the maximum of $|A|\cdot|B|$ over all edge bicliques, the empty ones included, so the hypothesis $a>0$ means $E\ne\emptyset$. The logarithm is natural (Real.log).

Conventions and readings committed to:

• The goal is stated for every optimal schedule, and the existence of an optimal schedule is a separate conclusion, so the bounds cannot hold vacuously. Proving the bounds for one particular schedule, or for an optimal value defined as an infimum that could be a junk default, would not be this lemma.
• No integrality hypothesis on $an$ is added.
• Milestones 2 and 3 are stated for every schedule (respectively every feasible schedule), not only for $\sigma^*$; milestone 1 states the value of the block-order schedule as an equality, where the paper writes "$\le\cdots=$".
• The paper's $P=(U\times V)\setminus E$ is irreflexive; feasibility only constrains distinct jobs, so it agrees with the reflexive partial order of §1.

Not formalized: Theorem 9.1 (cited hardness of maximum edge biclique) and Theorem 9.2 (no PTAS under a complexity assumption); no polynomial-time or complexity-theoretic statement appears in the mission. Contributions welcome: proofs of the three milestones and of the goal; Mathlib's bounds on harmonic numbers (Mathlib/NumberTheory/Harmonic/Bounds.lean) are the relevant library.

Selected references

• C. Ambühl, M. Mastrolilli, N. Mutsanas, O. Svensson, On the Approximability of Single-Machine Scheduling with Precedence Constraints, Mathematics of Operations Research 36(4):653–669, 2011. https://doi.org/10.1287/moor.1110.0512
• C. Ambühl, M. Mastrolilli, O. Svensson, Inapproximability results for sparsest cut, optimal linear arrangement, and precedence constraint scheduling, Proc. 48th IEEE FOCS, 329–337, 2007 (reference [4] of the paper).
• W. L. Eastman, S. Even, I. M. Isaacs, Bounds for the optimal scheduling of n jobs on m processors, Management Science 11(2):268–279, 1964 (reference [11]).
• M. X. Goemans, D. P. Williamson, Two-dimensional Gantt charts and a scheduling algorithm of Lawler, SIAM J. Discrete Math. 13(3):281–294, 2000 (reference [15]).
• P. Schuurman, G. J. Woeginger, Polynomial time approximation algorithms for machine scheduling: ten open problems, J. Scheduling 2(5):203–213, 1999 (reference [36]).

Motivation

In the single-machine scheduling problem $1|\mathrm{prec}|\sum w_jC_j$, a set $N$ of $n$ jobs, each with a processing time $p_j\ge 0$ and a weight $w_j\ge 0$, is processed on one machine without interruption, subject to precedence constraints given by a partial order $P$ on $N$. The aim is to minimize the weighted sum of completion times $\sum_j w_jC_j$. The problem is strongly NP-hard for general precedence constraints (Lawler 1978; Lenstra and Rinnooy Kan 1978), and its approximability was a recurring open question in scheduling theory (Schuurman and Woeginger 1999).

A line of work by Chudak and Hochbaum, Correa and Schulz, and Ambühl and Mastrolilli showed that the problem is a special case of minimum weighted vertex cover in a graph $G^S_P$ built from the instance. Many problems on partial orders become polynomial when the order is an interval order, so it is natural to ask whether this one does too. Section 7 of Ambühl, Mastrolilli, Mutsanas and Svensson (Math. Oper. Res. 2011) answers no: the problem stays NP-hard on interval orders. The proof is a reduction from vertex cover in connected graphs of maximum degree 3. This mission formalizes the correctness of that reduction.

Setting

A poset $P=(N,P)$ is read as a reflexive relation: $(x,y)\in P$ means $x\le y$. Jobs $x,y$ are incomparable if neither $(x,y)$ nor $(y,x)$ is in $P$, and $\operatorname{inc}(P)$ is the set of ordered incomparable pairs. The vertex cover graph $G^S_P$ has one node $(i,j)$ for each incomparable pair, weighted $p_iw_j$. Two nodes $(i,j)$ and $(k,\ell)$ are adjacent if $j=k$ and $i=\ell$, or $j=k$ and $(i,\ell)\in P$, or $(i,\ell)\in P$ and $(k,j)\in P$. Write $w(C_I)$ for the minimum weight of a vertex cover of $G^S_I$.

A poset is an interval order if each element $x$ can be assigned a closed real interval $[a_x,b_x]$ such that $x<y$ if and only if $b_x<a_y$.

The reduction starts from a graph $G=(V,E)$ with vertices $v_1,\dots,v_N$ and a spanning tree $T=(V,E_T)$ rooted at $v_1$, numbered so that each parent comes before its children. The paper uses a breadth-first search tree.

• Stage 1. The graph $G'$ is built from $T$. Each $v_i$ gets a pendant path $v_i - u^i_1 - u^i_2$. Each non-tree edge $\{v_i,v_j\}\in E\setminus E_T$ with $i<j$ gets the path $v_i - e^{ij}_1 - e^{ij}_2 - u^j_2$. The non-tree edges themselves are not edges of $G'$.
• Stage 2. The scheduling instance $S$ has jobs $s_0$, $s_1,\dots,s_N$, $m_1,\dots,m_N$, $e_1,\dots,e_N$, and $b_{ij}$ for each non-tree edge. Their intervals, processing times and weights are given in a table on p. 662. For example, $s_j$ has interval $[i,j]$, processing time $1/k^j$ and weight $k^i$, where $v_i$ is the parent of $v_j$. The precedence constraints $I$ are the interval order of these intervals. With $n$ the number of jobs, the parameter is $k=n^2+1$.
• The set $D$. It is $\{(s_0,s_1)\}\cup\{(s_i,s_j): v_i \text{ parent of } v_j\}\cup\{(s_i,m_i),(m_i,e_i)\}\cup\{(s_i,b_{ij}),(b_{ij},m_j)\}$. The graph $G'_I$ is the subgraph of $G^S_I$ induced by $D$.