OAI.SingleFold.main

The theorem states that the proposition MainStatement holds, which asserts a single-fold Diophantine representation result with positive lengths. For every n ≥ 1 and every set S of n-tuples of natural numbers that is recursively enumerable (the predicate a ∈ S is REPred, i.e. semi-decidable), there exist m ≥ 1 and an integer polynomial P in the n input variables and m witness variables such that P represents S. Here evaluation takes natural-number inputs a and witnesses w, casts them to integers, and evaluates P over ℤ. Representation means that for every input a, first, a lies in S exactly when some witness w ∈ ℕ^m satisfies P(a,w)=0, and second, any two witnesses w and v with P(a,w)=0 and P(a,v)=0 are equal. So there is exactly one witness for members of S and none for nonmembers, and the uniqueness condition is imposed on every input a, with all witness coordinates included in w. The statement is admitted with sorry in the source, not proved there.