OAI.LargeIndependentSets.mainTheoremReal

The theorem states that for every real δ with 0<δ<1/3, a RealGraphReduction δ exists (the type is nonempty); it is admitted without proof in the source. Such a reduction consists of a map from bit strings to graphs, where a graph is a nonempty finite simple undirected loopless graph on n vertices with a symmetric Boolean adjacency matrix. The map is computed in polynomial time by a multi-stack Turing machine (TM2 model), taking the input bit string unchanged and producing the full row-major adjacency matrix encoding of the graph, preceded by the binary vertex count, with every stack alphabet of the machine finite. In addition there is a polynomial over ℕ such that, for every input b, the length of the output encoding is at most that polynomial evaluated at the length of b. Formulas are lists of clauses, each a list of at most three literals (a variable index in ℕ with a sign), encoded in binary by framing each payload bit with a leading true and ending with false, and listing clause count, then each clause's length and literals. Completeness: whenever a formula is satisfiable, the graph obtained from its encoding is 3-colorable, meaning some coloring with three colors gives adjacent vertices different colors. Soundness: whenever a formula is unsatisfiable, the independence number of that graph, the size of its largest independent set, is strictly less than δ times its number of vertices.