Binary choices and polyhedral complexity

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

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

Polytopes, dimension, and facets

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

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

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

The growth target

The target is the following existence statement:

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

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

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

What superexponential growth says

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

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

Why the existence statement is demanding

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

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

Geometric conventions

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

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

Selected references

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

Recognizing a convex set from its projections

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

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

Sets, convex hulls, and affine projections

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

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

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

The recognition target

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

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

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

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

What the criterion establishes

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

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

Why the converse requires more than one image

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

Mathematical conventions

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

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

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

Selected references

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

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

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

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

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

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

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

$$A(P)=T\cap L.$$

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

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

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

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

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

Gale data and combinatorial type

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

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

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

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

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

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

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

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

Motivation

Edge-colored tournaments combine a complete orientation with a finite palette. They are a natural setting for comparing local multicolor obstructions with global directed reachability. The question attributed to Sands, Sauer, and Woodrow asks whether three colors force one of two outcomes: a directed triangle whose three arcs all have different colors, or a single vertex that can reach every target along a monochromatic directed path.

The problem was recorded by the Open Problem Garden in 2008. A minimum-counterexample reduction was later restated by Georgakopoulos and Sprüssel in their study of three-colored tournaments. The available project computation excludes counterexamples through eleven vertices, but that package is explicitly candidate_only: it is bounded search evidence, not a proof of the unrestricted theorem.

Setting

A tournament is an orientation of a finite complete simple graph. For each pair of distinct vertices $u,v$, exactly one of $u\to v$ and $v\to u$ is present. Every directed arc receives one of three labeled colors.

A rainbow directed triangle is a cyclically oriented triangle

$$a\to b\to c\to a$$

whose three arc colors are pairwise distinct. A transitive three-vertex subtournament is not a directed triangle and is therefore not forbidden merely because its three arcs have different colors.

A vertex $s$ is a monochromatic source when, for every vertex $t$, there is some color $k$ and a directed $s$-to-$t$ path all of whose arcs have color $k$. The chosen color may depend on $t$; the theorem does not demand one common color for all targets. Length-zero reachability handles $t=s$.

The formal domain is nonempty finite tournaments. This nonemptiness convention is stated explicitly because an empty vertex type has neither a rainbow triangle nor a candidate source and would trivialize the negation of the intended question.

Formalization targets

Root theorem

For every nonempty finite tournament $T$ with a three-coloring of its arcs,

$$T\text{ has a rainbow directed triangle} \quad\lor\quad \exists s\in V(T)\ \forall t\in V(T),\ \text{$s$ reaches $t$ monochromatically}.$$

No compatibility is required between the colors of paths to different targets, and unused palette colors are permitted.

Finite order milestone

The first milestone freezes the exact bounded claim supported by the replay package:

$$1\le |V(T)|\le 11\text{ and no rainbow directed triangle} \quad\Longrightarrow\quad T\text{ has a monochromatic source}.$$

The statement includes all tournaments and all three-color arc assignments at those orders, not only one symmetry representative. The repository's observations report exhaustive search after a minimum-counterexample reduction, but the Lean theorem remains open until it has an accepted proof.

Significance

The root theorem would turn a local forbidden configuration into a global reachability certificate. Such a result clarifies how orientation and edge color interact: ordinary Gallai decompositions for undirected colored complete graphs cannot be imported unchanged, because the hypothesis forbids only rainbow cyclic triangles and allows rainbow transitive triples.

The formal development creates reusable definitions for colored directed reachability and exposes the direction of every relation. This matters in minimum-counterexample arguments, where an auxiliary arc $u\to_F v$ may encode that $v$ cannot reach $u$; reversing that convention invalidates the cycle reduction. A verified finite milestone would also provide a regression target for SAT, SMT, or exhaustive encodings without elevating their raw output to a universal theorem.

Difficulty

The classical Gallai theorem is not directly applicable. It assumes an undirected complete graph with no rainbow triangle of any orientation, whereas this problem permits a transitive triple with three distinct colors. A proposed partition must therefore control both arc colors and directions between parts.

The minimum-counterexample route yields a useful spanning cycle in an auxiliary nonreachability digraph. It does not itself bound the size of a counterexample. The order-eleven computation terminates because its domain is finite, but no induction from eleven to arbitrary order follows. A proof must add a structural theorem that survives all orientations and allows monochromatic paths of arbitrary length rather than treating reachability bits as independent physical arcs.

Formalization scope

Lean represents the tournament as a binary relation D with looplessness and exactly one orientation on each unordered pair. The coloring is a total function on ordered pairs, but only values on actual arcs are semantically used. Monochromatic reachability is the reflexive transitive closure of arcs of one fixed color. The root and finite theorem quantify over every nonempty finite vertex type.

The finite replay, its solver versions, hashes, and no-witness observations remain external candidate evidence. They do not close the milestone without a checkable certificate or a proof accepted by the platform. Contributions may formalize the minimum-counterexample cycle lemma, build an independently checked finite certificate, isolate a directed decomposition theorem, or prove the root. No contribution may replace a directed rainbow triangle by an undirected one, require the same path color for every target, or assume heredity of failure for arbitrary induced subtournaments.

Selected references

• Open Problem Garden, Monochromatic reachability versus rainbow triangles, posted 2008. https://www.openproblemgarden.org/op/monochromatic_reachability_vs_rainbow_triangles
• B. Sands, N. Sauer, and R. Woodrow, On monochromatic paths in edge-coloured digraphs, Journal of Combinatorial Theory, Series B 33 (1982), 271–275.
• A. Georgakopoulos and P. Sprüssel, On 3-coloured tournaments, 2009. https://arxiv.org/abs/0904.1967
• A. Trygub, Full Characterization of Color Degree Sequences in Complete Graphs Without Tricolored Triangles, 2023. https://arxiv.org/abs/2304.14579

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$

$$\sum_{C \ni x} f(C) \le c(x), \qquad \sum_{C \ni e} f(C) \le c(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$:

$$G \text{ is } n\text{-tuply connected} \iff \text{for all } p_s \ne p_k,\ G \text{ has } n \text{ disjoint paths from } p_s \text{ to } p_k.$$

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

In binary classification the VC dimension decides PAC learnability: a class of $\{0,1\}$-valued functions is learnable from finitely many examples exactly when its VC dimension is finite. Multiclass classification, where a predictor outputs one of many labels, arises whenever the label set is large: language models choosing a next token, image recognition over open vocabularies, structured prediction. For finitely many labels the Natarajan dimension plays the role of the VC dimension (Natarajan 1989; Ben-David, Cesa-Bianchi, Haussler and Long 1995). Whether it still characterizes learnability when the label set is infinite stayed open for three decades.

Brukhim, Carmon, Dinur, Moran and Yehudayoff (arXiv:2203.01550, FOCS 2022) settled both directions. Their Theorem A shows that the DS dimension of Daniely and Shalev-Shwartz (COLT 2014, PMLR 35) characterizes multiclass PAC learnability for every label set. Their Theorem 2, the goal of this mission, shows that the Natarajan dimension does not: there is a class whose Natarajan dimension is $1$ and whose DS dimension is infinite.

Timeline:

• 1989: Natarajan introduces his dimension and proves it gives sample-complexity bounds when the label set is finite.
• 1995: Ben-David, Cesa-Bianchi, Haussler and Long show that, for finite label sets, every "reasonable" extension of the VC dimension characterizes learnability.
• 2003: Januszkiewicz and Świątkowski construct, for every dimension, finite simplicial complexes without empty squares from coset complexes of finite groups (Comment. Math. Helv. 78(3), 555–583); the multiclass paper uses this construction for its separation.
• 2014: Daniely and Shalev-Shwartz introduce the DS dimension, prove that finite DS dimension is necessary for learnability, and ask whether it is sufficient.
• 2022: Brukhim et al. prove that finite DS dimension is sufficient and that the Natarajan dimension fails to characterize learnability for infinite label sets.

Setting

A concept class is a set $\mathcal H \subseteq \mathcal Y^{\mathcal X}$ of functions from a domain $\mathcal X$ to a label set $\mathcal Y$, with no finiteness assumption on either. For a sequence $S = (x_1, \dots, x_n) \in \mathcal X^n$, the projection $\mathcal H|_S \subseteq \mathcal Y^n$ is the set of words $(h(x_1), \dots, h(x_n))$, $h \in \mathcal H$.

• $S$ is N-shattered if there are $f, g : [n] \to \mathcal Y$ with $f(i) \ne g(i)$ for every $i$ and $\mathcal H|_S \supseteq \{f(1), g(1)\} \times \dots \times \{f(n), g(n)\}$: the projection contains a copy of the Boolean cube. The Natarajan dimension $d_N(\mathcal H)$ is the largest $n$ for which some $S \in \mathcal X^n$ is N-shattered, or $\infty$.
• A pseudo-cube of dimension $d$ is a non-empty, finite $B \subseteq \mathcal Y^d$ in which every word $h$ has, for every coordinate $i$, an $i$-neighbour: a word $g \in B$ with $g(i) \ne h(i)$ and $g(j) = h(j)$ for $j \ne i$. $S$ is DS-shattered if $\mathcal H|_S$ contains an $n$-dimensional pseudo-cube, and the DS dimension $d_{DS}(\mathcal H)$ is the largest such $n$, or $\infty$.

Every Boolean cube is a pseudo-cube, so $d_N \le d_{DS}$. The hexagon $\{12, 32, 34, 54, 56, 16\} \subseteq \{1,\dots,6\}^2$ is a 2-dimensional pseudo-cube that contains no Boolean square.

The milestones pass through simplicial complexes: downward-closed families of finite sets. A complex is good if it is finite, pure, has a proper coloring $r$ of its vertices with $\dim(C)+1$ colors, and satisfies replacement (every vertex of every face can be exchanged for a new vertex). A good complex $C$ with coloring $r$ defines the class $B(C, r)$ of its top faces, each written as the word listing its vertices by color. A square is a 4-cycle of distinct vertices in the 1-skeleton; it is empty if neither diagonal is an edge. The coset complex $C_F(H_1, \dots, H_d)$ of subgroups of a group $F$ has the cosets $gH_i$ as vertices and the sets of cosets with a common point as faces.

Formalization targets

Goal: Theorem 2 (p. 4)

$$\exists\, \mathcal X, \mathcal Y,\ \mathcal H \subseteq \mathcal Y^{\mathcal X}:\qquad d_N(\mathcal H) = 1 \quad\text{and}\quad d_{DS}(\mathcal H) = \infty.$$

Milestones

1. Theorem 45 (p. 30; Januszkiewicz–Świątkowski): for every $d > 1$ a finite group $F$ and subgroups $H_1, \dots, H_d$ with $(\bigcap_{j\ne i} H_j) \setminus H_i \ne \emptyset$ for all $i$, whose coset complex has no empty squares.
2. Proposition 46 (p. 31): such a coset complex has dimension $d - 1$, is good and has no empty squares.
3. Proposition 42 (p. 28): a $d$-dimensional good complex with a proper coloring $r$ yields the $(d+1)$-dimensional pseudo-cube $B(C, r)$; conversely every pseudo-cube yields a good complex $C(B)$.
4. Proposition 43 (p. 29): $d_N(B(C,r)) \ge 2$ iff $C$ has a square $v_0 v_1 v_2 v_3$ with $r(v_0) = r(v_2)$ and $r(v_1) = r(v_3)$.
5. Corollary 44 (p. 29): a good complex without empty squares gives $d_N(B(C, r)) \le 1$ for every proper coloring.
6. Proof of Theorem 2 (p. 32): for every $d \ge 1$, a $d$-dimensional pseudo-cube with Natarajan dimension exactly $1$.

Significance

Theorem 2 shows that the classical generalization of the VC dimension to many labels is the wrong invariant once the label set is infinite: a class can contain no Boolean square at all and still be unlearnable, because it contains pseudo-cubes of every dimension. Combined with the necessity of finite DS dimension, it gives a class that is not PAC learnable although its Natarajan dimension is $1$, and it identifies pseudo-cubes, not Boolean cubes, as the relevant combinatorial obstruction. It also links learning theory to a problem studied in geometric group theory, finite "flag-no-square" complexes.

The paper's proof is complete modulo Theorem 45, which it imports from Januszkiewicz–Świątkowski 2003. None of these results is formalized. A formalization would give machine-checked versions of the dictionary between concept classes and properly colored complexes (Propositions 42–44), of the coset-complex translation (Proposition 46), and of the final disjoint-union argument; Theorem 45 itself, which rests on Coxeter-group and topological arguments, is a separate and substantial formalization target.

Difficulty

Infinite complexes that are pure, properly colored, satisfy replacement and have no empty squares are easy to build: grow a tree of faces indefinitely. The definition of a pseudo-cube demands finiteness, and the difficulty is entirely there: one must "fold" such an infinite object into a finite one without creating an empty square. The obvious finite candidate, the group $(\mathbb Z/2)^d$ with its coordinate subgroups, produces the Boolean cube, whose complex is full of empty squares. Theorem 45 is the input that resolves this, and it is far beyond the rest of the argument.

Formalization scope

All declarations live in the namespace MulticlassDS.NatGap.

• Concept classes are Set (X → Y) with arbitrary types; $[n]$ is Fin n (0-based), and shattering is defined for sequences Fin n → X, as in the paper.
• Both dimensions are ℕ∞-valued suprema, so "infinite DS dimension" is dsDim H = ⊤. An ℕ-valued supremum would silently return $0$ on an unbounded family and would trivialize the goal.
• The goal requires the Natarajan dimension to be exactly $1$; an upper bound alone holds for any class with at most one element.
• Pseudo-cubes are required to be finite (Definition 5). Without finiteness, the tree classes of Example 8 would already have infinite "DS dimension".
• Complexes are Set (Finset V). The dimension is the predicate HasDim C d, not a natural-number subtraction, and colors are Fin (d + 1).
• Replacement is stated with a new vertex $u \notin f$. The page writes "$u \ne v$", but read literally that allows $u \in f$, which makes the condition hold by downward closure and makes Proposition 42 false; the proofs of Propositions 42 and 46 use a new vertex.
• Coset-complex vertices are left cosets as subsets of the group, not pairs (index, coset).
• Proposition 46 states dimension $d - 1$ under $d > 1$, where the subtraction is exact; the converse of Proposition 42 is indexed by $d + 1$ and $d$ to avoid it.
• The proof-of-Theorem-2 milestone says "for every $d$"; it is posed for $d \ge 1$, because at $d = 0$ the only pseudo-cube has Natarajan dimension $0$.

Welcome contributions: proofs of Propositions 42–44 and 46 and of the goal from the milestones, which need only finite combinatorics and elementary group theory; and, separately, a formalization of the Januszkiewicz–Świątkowski construction behind Theorem 45. The definitions of pseudo-cubes, the DS dimension and good complexes are reusable by the companion mission on sample compression and by any later work on multiclass learnability.

Selected references

• N. Brukhim, D. Carmon, I. Dinur, S. Moran, A. Yehudayoff, A Characterization of Multiclass Learnability, arXiv:2203.01550v1, 2022 (FOCS 2022). https://arxiv.org/abs/2203.01550
• T. Januszkiewicz, J. Świątkowski, Hyperbolic Coxeter groups of large dimension, Comment. Math. Helv. 78(3) (2003), 555–583 (reference [Januszkiewicz and Świątkowski 2003] of arXiv:2203.01550v1, p. 33).
• A. Daniely, S. Shalev-Shwartz, Optimal learners for multiclass problems, COLT 2014, PMLR 35, 287–316. https://proceedings.mlr.press/v35/
• B. K. Natarajan, On learning sets and functions, Machine Learning 4 (1989), 67–97. https://doi.org/10.1007/BF00114804
• S. Ben-David, N. Cesa-Bianchi, D. Haussler, P. M. Long, Characterizations of learnability for classes of {0,…,n}-valued functions, J. Comput. Syst. Sci. 50(1) (1995), 74–86. https://doi.org/10.1006/jcss.1995.1008

Motivation

In multiclass classification a learner sees examples $(x, y)$ with $x$ in a domain $\mathcal X$ and a label $y$ in a set $\mathcal Y$, and must predict labels of new points. When $\mathcal Y$ is finite, the Natarajan dimension characterizes PAC learnability, extending the role of the VC dimension in binary classification (Natarajan 1989; Ben-David, Cesa-Bianchi, Haussler, Long 1995). Label sets in practice are often unbounded: structured prediction, ranking, and language modelling all predict from very large or infinite label spaces. For infinite $\mathcal Y$ the Natarajan dimension fails to characterize learnability, and the question of which combinatorial parameter does was left open by Daniely and Shalev-Shwartz.

Timeline:

• 1989–1995. Natarajan, then Ben-David et al. and Haussler–Long: for finite $\mathcal Y$, learnability is equivalent to finite Natarajan dimension, with sample complexity depending on $\log|\mathcal Y|$.
• 2011–2015. Daniely, Sabato, Ben-David and Shalev-Shwartz show that ERM can fail for multiclass problems with many labels. Daniely and Shalev-Shwartz (COLT 2014) introduce the DS dimension, prove that finite DS dimension is necessary for learnability, and ask whether it is sufficient.
• 2022. Brukhim, Carmon, Dinur, Moran, Yehudayoff prove sufficiency, so the DS dimension characterizes multiclass PAC learnability, and show that the Natarajan dimension does not.

Setting

A concept class is a set $\mathcal H\subseteq\mathcal Y^{\mathcal X}$ of functions. For a sequence $S=(x_1,\dots,x_n)$ the projection $\mathcal H|_S\subseteq\mathcal Y^n$ is the set of label words $(h(x_1),\dots,h(x_n))$, $h\in\mathcal H$. A finite non-empty set $B\subseteq\mathcal Y^d$ is a pseudo-cube if every $h\in B$ has, in every coordinate $i$, a neighbour $g\in B$ that differs from $h$ exactly in coordinate $i$. The sequence $S$ is DS-shattered if $\mathcal H|_S$ contains an $n$-dimensional pseudo-cube, and the DS dimension $d_{DS}(\mathcal H)$ is the maximum length of a DS-shattered sequence. The Natarajan dimension $d_N(\mathcal H)\le d_{DS}(\mathcal H)$ is the same with Boolean cubes $\prod_i\{f(i),g(i)\}$, $f(i)\ne g(i)$, in place of pseudo-cubes.

A sample $S\in(\mathcal X\times\mathcal Y)^n$ is $\mathcal H$-realizable if some $h\in\mathcal H$ is consistent with it. An $n\to r$ sample compression scheme for $\mathcal H$ (Littlestone and Warmuth 1986) is a single reconstruction function $\rho:(\mathcal X\times\mathcal Y)^r\to\mathcal Y^{\mathcal X}$ such that every realizable sample of size $n$ contains $r$ of its examples $S'$ with $\rho(S')$ consistent with the whole sample. Logarithms are base $2$ throughout.

Formalization targets

Goal: Theorem 36 (p. 22)

For $\mathcal H$ with $d_{DS}(\mathcal H)=d_{DS}<\infty$ and $d_N(\mathcal H)=d_N$, and all integers $n,t>0$, there is an $n\to r$ sample compression scheme, $r\le n$, with

$$r\le\left(\frac{d_{DS}+t+1}{t+1}(d_{DS}+t)+10^3d_N\log\left(\binom{d_{DS}+t+1}{t+1}\log(2n)\right)\right)\log(2n).$$

Milestones

The scheme combines two components, each with its own chain of results:

• List learning from the DS dimension. Lemma 13 (orientations of out-degree $\le d$ on $\mathcal Y^{d+1}$), Claim 16 (the one-inclusion algorithm is right on some leave-one-out example), Fact 14 (leave-one-out symmetrization), Proposition 32 (a list PAC learner with list size $\binom{d+t}{t}$ and success probability $\frac{t+1}{d+t+1}$), Lemma 39 (an $n\to r_1$ list compression scheme with $r_1\le\frac{d_{DS}+t+1}{t+1}(d_{DS}+t)\log(2n)$ and menu size $\le\binom{d_{DS}+t+1}{t+1}\log(2n)$).
• Learning from a menu via shifting. Claim 22, Corollary 23, Claim 26, Proposition 27 ($\operatorname{avd}\le4d_E$), Corollary 28, Lemma 29 ($d_E\le5d_N\log p$), Lemma 17 (orientations of out-degree $\le20d_N\log p$ on $[p]^n$), Proposition 34 (error $\le20d_N\log(p)/n$ given a $p$-menu), Lemma 40 (an $n\to r_2$ compression scheme given a $p$-menu with $r_2\le10^3d_N\log(p)\log(2n)$).

Significance

Theorem 36 is the algorithmic heart of the characterization: by the standard "compression implies generalization" argument it gives PAC learnability of every class of finite DS dimension, with sample complexity $\tilde O(d_{DS}^{3/2}/\epsilon)$ in the realizable case ($t=\lceil d_{DS}^{1/2}\rceil$), and with the agnostic case following by known reductions. It also exhibits sample compression schemes of size polylogarithmic in $n$ for multiclass classes with infinitely many labels, in contrast to the constant-size schemes known for finite VC classes.

The result is proved in the paper; none of it is formalized. The formalization would produce a machine-checked theory of one-inclusion graphs and their orientations, multiclass shifting, the exponential dimension, list learning, and sample compression schemes for arbitrary label sets. These objects recur throughout learning theory (one-inclusion graphs in optimal PAC learning, shifting in VC theory), so the infrastructure is reusable beyond this mission.

Difficulty

The natural first idea, running empirical risk minimization or bounding the Natarajan dimension, fails: classes with Natarajan dimension $1$ and infinitely many labels can be unlearnable, and ERM can fail even for learnable classes. The DS dimension gives only a weak guarantee: by Claim 16, among $d+1$ leave-one-out runs, one is correct. Turning this into a learner requires a list learner whose menus are still of unbounded total size, and then learning with a menu of size $p$, where the obstacle is controlling one-inclusion graph orientations over $[p]^n$ by the Natarajan dimension. Multiclass shifting does not preserve the average degree (Example 20), so the binary argument breaks down, and a new potential ($\operatorname{avd}'$) and a new dimension ($d_E$) are needed. Lemma 13 for infinite classes needs a compactness argument.

Formalization scope

Lean conventions:

• A class is H : Set (X → Y) with arbitrary types X, Y; sequences and samples are functions on Fin n ($[n]$ is 0-based).
• The DS, Natarajan and exponential dimensions are suprema in ℕ∞, so unbounded families give ⊤; hypotheses are written dsDim H = dDS with dDS : ℕ. A pseudo-cube is required to be finite.
• Logarithms are Real.logb 2. Menu sizes use Set.encard.
• A compression scheme is a reconstruction function fixed before the sample (∃ ρ, ∀ S, ∃ S'); a subsample may repeat and reorder examples. Theorem 36 states $r\le n$ explicitly.
• Orientations of the one-inclusion graph of $V\subseteq\mathcal Y^m$ are maps sending a direction $i$ and a vertex $v$ to the head of the edge of direction $i$ through $v$; the out-degree of $v$ counts directions whose head is not $v$.
• Classes over $[p]$ use labels Fin p; the shifting condition $1\le g(i)\le|e_f|$ becomes $g(i)<|e_f|$.
• The one-inclusion algorithm (Algorithms 1 and 3) is parametrized by a permutation-equivariant choice of minimal orientations, the reading under which the paper's leave-one-out proofs are valid; statements about the algorithm hold for every such choice. Its default output on non-realizable input requires a non-empty label set, assumed in Claim 16 and Propositions 32 and 34. Lemma 40 assumes a non-empty label set because it is false for $\mathcal X\ne\emptyset=\mathcal Y$.
• Distributions are discrete (PMF), and i.i.d. probabilities are sums over $\mathcal Z^m$. The measure-theoretic generality of the paper is not attempted.

A trivial formalization is ruled out by these choices. Placing the reconstruction function after the sample would let it output the consistent hypothesis. A dimension in ℕ defined by sSup would be $0$ for infinite dimension. Pseudo-cubes without finiteness would change the dimension (Example 8).

Contributions welcome: proofs of any milestone, in particular the shifting results of §3 (self-contained combinatorics on finite classes), Fact 14 (pure discrete probability), and Lemma 13; general-purpose lemmas about one-inclusion graphs, orientations and sample compression schemes are reusable by other learning-theory missions.

Selected references

• N. Brukhim, D. Carmon, I. Dinur, S. Moran, A. Yehudayoff, A Characterization of Multiclass Learnability, FOCS 2022; arXiv:2203.01550v1 (2022). https://arxiv.org/abs/2203.01550
• A. Daniely, S. Shalev-Shwartz, Optimal Learners for Multiclass Problems, COLT 2014. https://arxiv.org/abs/1405.2690
• N. Littlestone, M. Warmuth, Relating Data Compression and Learnability, unpublished technical report, University of California, Santa Cruz, 1986 (no stable link).
• D. Haussler, N. Littlestone, M. Warmuth, Predicting {0,1}-Functions on Randomly Drawn Points, Information and Computation 115(2), 1994. https://doi.org/10.1006/inco.1994.1097
• D. Haussler, P. M. Long, A Generalization of Sauer's Lemma, Journal of Combinatorial Theory, Series A 71(2), 1995. https://doi.org/10.1016/0097-3165(95)90006-3
• S. Ben-David, N. Cesa-Bianchi, D. Haussler, P. M. Long, Characterizations of Learnability for Classes of {0,…,n}-Valued Functions, JCSS 50(1), 1995. https://doi.org/10.1006/jcss.1995.1008
• B. K. Natarajan, On Learning Sets and Functions, Machine Learning 4, 1989. https://doi.org/10.1007/BF00114804

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

$$P=(U\times V)\setminus E,$$

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

$$n^2-an^2\Bigl(\ln\frac1a+2\Bigr)\le\mathrm{val}(\sigma^*)\le n^2-an^2 .$$

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

$$\mathrm{val}(\sigma)=n^2-|A|\cdot|B| .$$

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

$$\mathrm{val}(\sigma)=\sum_{i=1}^n\bigl(\sigma(i+1)-\sigma(i)\bigr)i=n^2-\sum_{i=1}^n\sigma(i).$$

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

$$\sigma(i)(n-i+1)\le an^2,\qquad \sigma(i)\le 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

Single-machine scheduling with precedence constraints, written $1|\mathrm{prec}|\sum w_jC_j$ in the notation of Graham et al., asks for an order of $n$ weighted jobs on one machine that respects a given partial order and minimizes the weighted sum of completion times. The problem is strongly NP-hard (Lawler 1978; Lenstra and Rinnooy Kan 1978), and closing its approximability gap is listed by Schuurman and Woeginger among ten outstanding open problems in scheduling theory. Several 2-approximation algorithms are known (Schulz 1996; Hall et al. 1997; Chudak and Hochbaum 1999; Chekuri and Motwani 1999; Margot et al. 2003).

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 built from the precedence order. Ambühl, Mastrolilli, Mutsanas and Svensson (Math. Oper. Res. 36(4), 2011) observed that this graph is the graph of incomparable pairs of dimension theory, and used that identification to obtain $(2-2/f)$-approximations for orders of fractional dimension at most $f$. This mission formalizes that framework: the identification of the two graphs and the rounding guarantee of the paper's Theorem 5.1.

Setting

An instance $S$ consists of a finite set $N$ of jobs, a partial order $P$ on $N$ (reflexive, antisymmetric, transitive; $(i,j)\in P$ with $i\ne j$ means job $i$ finishes before job $j$ starts), processing times $p_j\ge 0$ and weights $w_j\ge 0$.

Two jobs $x,y$ are incomparable, $x\parallel y$, when neither $(x,y)$ nor $(y,x)$ lies in $P$. The set $\operatorname{inc}(P)$ of incomparable pairs consists of ordered pairs and is closed under swapping. A linear extension of $P$ is a linear order $L\supseteq P$ on $N$; it reverses $(x,y)\in\operatorname{inc}(P)$ when $y<x$ in $L$. A nonempty multiset $L_1,\dots,L_t$ of linear extensions is a $k:t$-realizer if every incomparable pair is reversed by at least $k$ of them. The fractional dimension $\operatorname{fdim}(P)$ is the least ratio $t/k$ over all $k:t$-realizers.

The vertex cover graph $G^S_P$ has the incomparable pairs as nodes; 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),(k,j)\in P$ (symmetrically closed). Node $(i,j)$ has weight $w_{(i,j)}=p_iw_j$, and $w(C)=\sum_{u\in C}w_u$. $\mathrm{OPT}$ is the minimum weight of a vertex cover of $G^S_P$. The LP relaxation [CS-LP] asks for $x\in[0,1]^{\operatorname{inc}(P)}$ with $x_u+x_v\ge1$ on every edge, minimizing $\sum_u w_ux_u$. For a solution $x$ write $V_a=\{u: x_u=a\}$, and for a linear extension $L$ let $I_{1/2}(L)$ be the pairs of $V_{1/2}$ reversed in $L$.

The graph of incomparable pairs $G_P$ (Felsner and Trotter 2000) also has the incomparable pairs as vertices; two of them are adjacent when the pair of them is a minimal set of incomparable pairs that no linear extension reverses entirely.

Formalization targets

Goal: Theorem 5.1 (p. 658)

For an instance $S$, a $k:t$-realizer $L_1,\dots,L_t$ of $P$, and a half-integral optimal solution $x$ of [CS-LP], put $C_i=V_1\cup\bigl(V_{1/2}\setminus I_{1/2}(L_i)\bigr)$. Then every $C_i$ is a vertex cover of $G^S_P$, and

$$\frac1t\sum_{i=1}^t w(C_i)\;\le\;\Bigl(2-\frac{2}{t/k}\Bigr)\mathrm{OPT}.$$

Milestones

• Proposition 3.2 (p. 657): $G^S_P=G_P$.
• Footnote 4 (p. 659): the pairs reversed by a linear extension are independent in $G^S_P$.
• Eq. (4): $\frac1t|\{i: L_i\text{ reverses }u\}|\ge k/t$ for every incomparable pair $u$.
• Eq. (5): $\frac1t\sum_i w(I_{1/2}(L_i))\ge \frac kt\,w(V_{1/2})$.
• Hochbaum's observation (§5, p. 659): for half-integral feasible $x$, $V_1\cup C$ covers $G^S_P$ whenever $C$ covers $G^S_P[V_{1/2}]$.
• Eqs. (6)–(8): $\frac1t\sum_iw(C_i)\le w(V_1)+(1-\frac kt)w(V_{1/2})\le 2(1-\frac kt)(w(V_1)+\frac12w(V_{1/2}))\le(2-\frac2{t/k})\mathrm{OPT}$ when $P$ is not a linear order.

Significance

The result. Combined with the cited Theorem 2.1 (Ambühl–Mastrolilli 2009; Correa–Schulz 2005), which turns an $\alpha$-approximate vertex cover of $G^S_P$ into an $\alpha$-approximate schedule, Theorem 5.1 gives a $(2-2/f)$-approximation for $1|\mathrm{prec}|\sum w_jC_j$ whenever the precedence order has an efficiently samplable realizer with $t/k\le f$. The paper applies it to interval orders ($3/2$), convex bipartite orders and semiorders ($4/3$), orders of bounded degree and orders of interval dimension two; for the earlier special classes it matched or improved the best known ratios, and for the last two it gave the first results. Proposition 3.2 makes the dimension theory of posets (realizers, critical pairs, fractional dimension) directly available to the vertex cover approach.

Formalizing it. The results are proved in the paper; to the best of current knowledge none of them has a machine-checked proof. The mission produces a Lean development of incomparable pairs, linear extensions, $k$-fold realizers and the hypergraph of incomparable pairs, which other dimension-theory missions can reuse, and a verified LP-rounding argument for half-integral vertex cover solutions under a distribution of independent sets.

Difficulty

Most of the rounding argument is arithmetic over finite sums. The central nontrivial step is the inclusion $G_P\subseteq G^S_P$ in Proposition 3.2: for two incomparable pairs that are not adjacent under the three-case rule, one must construct a single linear extension reversing both. This needs an extension of $P$ by two new comparabilities whose transitive closure is still antisymmetric, followed by Szpilrajn's theorem; checking that every potential cycle is excluded by the three cases is the actual content. The opposite inclusion, and footnote 4, follow from transitivity and antisymmetry of linear orders. A second point of care is the inequality $t\ge 2k$ used in step (7): it is not part of the definition of a realizer, and follows from each linear extension reversing exactly one of $(x,y)$ and $(y,x)$.

Formalization scope

• Jobs form a finite type N; the precedence order is a relation P : N → N → Prop with IsPartialOrder, carried by the structure Instance. Processing times and weights are nonnegative reals.
• $\operatorname{inc}(P)$ is the subtype IncPair P of N × N; a linear extension is a relation with IsLinearOrder containing P; a $k:t$-realizer is a family Fin t → LinearExtension P with $t>0$. Reversal of $(x,y)$ means $y<x$ in $L$ throughout; the page's "$y>x$" in Eq. (4) and "$\mathrm{Prob}[j>i]$" in Eq. (5) are the same family of inequalities because $\operatorname{inc}(P)$ is symmetric.
• $G^S_P$ is the symmetric closure of the printed three-case rule on distinct nodes. $G_P$ is defined through linear extensions and hyperedge minimality, never through the three-case rule, so Proposition 3.2 is a genuine statement and not a definitional equality.
• [CS-LP] drops the constant term $\sum_jp_jw_j+\sum_{(i,j)\in P}p_iw_j$ of [CS-IP], which does not affect optimality. $\mathrm{OPT}$ is the minimum weight of a vertex cover of $G^S_P$, taken over a finite nonempty family.
• Not formalized: "efficiently samplable", "polynomial time" and "randomized algorithm". The expectation over a uniformly sampled $L_i$ is stated as the average $\frac1t\sum_{i=1}^t$, which is equivalent to it and stronger than the existence of one good index. The existence of a half-integral optimal [CS-LP] solution (Nemhauser–Trotter, cited) is a hypothesis on $x$. The conversion of a vertex cover into a schedule (Theorem 2.1, cited) is not formalized; the goal is stated for vertex covers of $G^S_P$.
• Constants: $2-2/(t/k)$ in real arithmetic; it equals $2-2k/t$, and equals $2$ when $k=0$.
• The paper assumes $\operatorname{fdim}(P)\ge2$, i.e. $P$ is not a linear order. Eqs. (6)–(8) carry that hypothesis as the paper does; the goal omits it because for a linear order both sides are $0$.
• Conclusion (a), that each $C_i$ is a vertex cover, is part of the goal and is not assumed.

Contributions welcome: proofs of the milestones in any order, and a reusable Szpilrajn-style lemma producing a linear extension that reverses a prescribed set of compatible incomparable pairs.

Selected references

• C. Ambühl, M. Mastrolilli, N. Mutsanas, O. Svensson, On the approximability of single-machine scheduling with precedence constraints, Math. Oper. Res. 36(4):653–669, 2011. https://doi.org/10.1287/moor.1110.0512
• C. Ambühl, M. Mastrolilli, Single machine precedence constrained scheduling is a vertex cover problem, Algorithmica 53(4), 2009 (reference [2] of the paper).
• J. R. Correa, A. S. Schulz, Single-machine scheduling with precedence constraints, Math. Oper. Res. 30(4):1005–1021, 2005. https://doi.org/10.1287/moor.1050.0158
• G. R. Brightwell, E. R. Scheinerman, Fractional dimension of partial orders, Order 9(2):139–158, 1992 (reference [7]).
• S. Felsner, W. T. Trotter, Dimension, graph and hypergraph coloring, Order 17(2):167–177, 2000 (reference [13]).
• D. S. Hochbaum, Efficient bounds for the stable set, vertex cover and set packing problems, Discrete Appl. Math. 6(3):243–254, 1983 (reference [20]).
• G. L. Nemhauser, L. E. Trotter, Vertex packings: structural properties and algorithms, Math. Programming 8(1):232–248, 1975 (reference [29]).

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$.

Formalization targets

Goal: Theorem 7.1 (p. 661)

For every connected graph $G$ of maximum degree at most $3$, every parent-first spanning tree $T$ and every $m\in\mathbb N$, the precedence constraints $I$ of $S$ form an interval order, and

$$G \text{ has a vertex cover of size} \le m \iff \lfloor w(C_I)\rfloor \le m + |V| + |E\setminus E_T|.$$

Milestones, in the order the proof uses them

• Claim 1 (p. 662): $\tau(G') = \tau(G)+|V|+|E\setminus E_T|$, where $\tau$ is the vertex cover number.
• Remark 7.1 (p. 662): for jobs with intervals $[a,b]$ and $[c,d]$ and $a\le d$, $p_i\le 1/k^{\lceil b\rceil}$ and $w_j\le k^{\lceil c\rceil}$. On incomparable pairs $p_iw_j\in\{1\}\cup[0,1/k]$. Moreover, $p_iw_j\ge k$ forces $b<c$, and $p_iw_j=1$ forces $\lceil b\rceil=\lceil c\rceil$.
• Claim 2 (p. 663): an incomparable pair $(i,j)$ has $p_iw_j=1$ if it is in $D$, and $p_iw_j\le 1/k$ otherwise.
• Claim 3 (p. 663): $G'_I\cong G'$.
• §7, p. 664: with $k=n^2+1$, $\sum_{(i,j)\in\operatorname{inc}(I)\setminus D}p_iw_j<1$, and hence $w(C'_I)=\lfloor w(C_I)\rfloor$.

Significance

The result. Interval orders are a standard tractable class: several scheduling and order-theoretic problems that are hard in general become polynomial on them (Papadimitriou and Yannakakis 1979). Theorem 7.1 puts $1|\mathrm{prec}|\sum w_jC_j$ outside this pattern. Section 6 of the same paper shows that the problem nonetheless has a $3/2$-approximation on interval orders, so hardness and approximability are separated on this class. The paper also remarks that the proof makes weighted vertex cover NP-hard to approximate within some factor $r>1$ on the graphs $G^S_I$ arising from interval orders.

Formalizing it. The theorem is proved in the paper. Nothing in this mission is open, and none of it has been machine-checked before. The work splits into the following parts:

• a gadget argument on unweighted vertex covers (Claim 1, after Alimonti and Kann);
• an exact case analysis of incomparable pairs in a concrete interval order (Remark 7.1, Claim 2);
• a graph isomorphism (Claim 3);
• a rounding argument that links weighted and unweighted optima.

The definitions of $G^S_P$ and of minimum-weight vertex covers are shared with the other missions of this series.

Difficulty

The construction is explicit, and each step is elementary. The work is in the bookkeeping. Claim 2 requires classifying every incomparable pair of jobs, including pairs of different kinds such as $(b_{ij}, s_\ell)$, by comparing ceilings of interval endpoints. Half-integer endpoints ($m_i$, $b_{ij}$) are exactly what separates weight-one pairs from comparable ones. Claim 3 requires checking adjacency in $G^S_I$ for all pairs of nodes of $D$ in both directions. The paper writes out two cases in each direction and calls the rest similar.

Claim 1 has a direction that is not simply local. A vertex cover of $G'$ that misses both endpoints of a non-tree edge has to be repaired by swapping gadget vertices, and the repair must be repeated without increasing the size.

A natural first idea is to treat the light nodes (weight at most $1/k$) as negligible one at a time. This does not suffice: the argument needs their total weight to stay below $1$, which is what forces $k$ to grow with $n^2$.

Formalization scope

• Graph and tree. $G$ is a SimpleGraph (Fin N); vertex $v_{i+1}$ is i, and the root is index 0. The tree is a TreeLayout: a parent function returning none exactly at the root, with each parent of smaller index and adjacent in $G$. The statements hold for every such layout. This is stronger than the paper's breadth-first tree, and the proof uses only "parent before child".
• Hypotheses of the goal. Connectivity and the degree bound ((G.neighborSet v).ncard ≤ 3) are kept as in the paper. They matter only for the NP-completeness of the source problem.
• Jobs. The jobs form an inductive type with one constructor per row of the table. Their order is a PartialOrder instance: $x\le y$ iff $x=y$ or $b_x<a_y$. Processing times and weights are real numbers. Section 1 of the paper asks for nonnegative integers, but the instance uses $1/k^j$ and the formalization follows the instance as printed.
• Constants. The constants are explicit: $k=n^2+1$ with $n$ the cardinality of the job type, and $c=|V|+|E\setminus E_T|$. Remark 7.1 and Claim 2 are stated for every real $k>1$.
• Optimum values. $w(C_I)$ is a minimum over the finite family of vertex covers. Unweighted cover numbers are Mathlib's SimpleGraph.vertexCoverNum. The floor is Nat.floor, which agrees with the integer floor because $w(C_I)\ge 0$.
• Not formalized. The goal's wording ("NP-hard") is not formalized. Neither are the NP-completeness of degree-3 vertex cover (Garey, Johnson and Stockmeyer), the polynomial size of the construction, or Theorem 2.1 (cited), which turns a vertex cover of $G^S_I$ into a schedule. What is stated is the correctness of the reduction: the instance has interval-order constraints, and its optimum decides the vertex cover question.
• No trivialization. The instance $S$ is built from $G$ and $T$ exactly as in the table. The goal quantifies over all graphs and layouts, never over an instance $S$ assumed to have the properties.
• Contributions. Contributions are welcome on any milestone. Claims 1 and 3 are independent of the weights, and Claim 2 is independent of the graph theory.

Selected references

• C. Ambühl, M. Mastrolilli, N. Mutsanas, O. Svensson, On the Approximability of Single-Machine Scheduling with Precedence Constraints, Math. Oper. Res. 36(4):653–669, 2011. https://doi.org/10.1287/moor.1110.0512
• C. Ambühl, M. Mastrolilli, Single machine precedence constrained scheduling is a vertex cover problem, Algorithmica 53(4):488–503, 2009. https://doi.org/10.1007/s00453-008-9251-1
• J. R. Correa, A. S. Schulz, Single machine scheduling with precedence constraints, Math. Oper. Res. 30(4):1005–1021, 2005. https://doi.org/10.1287/moor.1050.0158
• P. Alimonti, V. Kann, Some APX-completeness results for cubic graphs, Theoret. Comput. Sci. 237(1–2):123–134, 2000. https://doi.org/10.1016/S0304-3975(98)00158-3
• M. R. Garey, D. S. Johnson, L. Stockmeyer, Some simplified NP-complete graph problems, Theoret. Comput. Sci. 1(3):237–267, 1976. https://doi.org/10.1016/0304-3975(76)90059-1
• C. H. Papadimitriou, M. Yannakakis, Scheduling interval-ordered tasks, SIAM J. Comput. 8(3):405–409, 1979. https://doi.org/10.1137/0208031