OAI.ThreeMachine.main_theorem

The theorem states that the defined proposition ReleaseTheorem holds (the proof is admitted, not given). That proposition asserts that there exist numbers k, q, g, a multitape Turing machine M with k+1 tapes, q+1 states and tape alphabet of size g+3 (a blank plus the two bit symbols for false and true, and g extra symbols), and a constant C>0, such that the following holds for every n≥1 and every directed graph G on the vertices Fin n, given as a list of edges, that is acyclic (no vertex lies on a nonempty directed path back to itself), and every optional deadline that is either absent or a value T with 1≤T≤n. There is a correct output out, and M, started in its initial state with the binary encoding of the pair (G, deadline) on tape 0 and the other tapes blank, halts within C·(L+2)^150020 steps, where L is the length of that encoded input, with tape 0 from the head position rightward holding exactly out. A schedule for G with horizon T is a map τ assigning each vertex a time slot in 1..T so that at most three vertices share any slot and every edge u→v has τ(u)<τ(v), which is three-machine unit-time scheduling with precedence constraints. Correct output means this. With no deadline, out encodes a feasible schedule τ, as the list of its slots, whose horizon T is minimal over all feasible horizons and schedules. With deadline T, out either encodes the answer none and no feasible schedule with horizon T exists, or out encodes some feasible schedule with horizon T.