OAI.VertexCover.every_fixed_factor_below_two

The theorem states that for every real number α with 1 ≤ α < 2, if there is an Approximation α, then the type ThreeSATDecision is nonempty. An Approximation α is a polynomial-time Turing-machine-computable (on a machine with finite alphabets) map run from explicit graphs to lists of natural numbers, where an explicit graph has n vertices and a duplicate-free list of edges (i,j) with i<j. For each graph G, the output list must have no repeated entries, contain only vertex indices below G.n, cover every edge (at least one endpoint appears in it), and have length at most α times the minimum vertex cover size of G. A ThreeSATDecision is a polynomial-time Turing-machine-computable (finite alphabets) function from bit strings to Booleans that returns true exactly on those inputs which decode, under the given binary encoding of 3-CNF formulas, to a satisfiable formula. So the statement is that any such α-approximation algorithm for vertex cover with α in [1,2) yields a polynomial-time decision procedure for 3-SAT.