CLIQUE is NP-complete

With no parameters, hypotheses, or typeclass assumptions, the declaration asserts that the following language $C$ of all finite Boolean strings is both in NP and NP-hard under the precise machine and encoding conventions described here. Identify false and true with the bits $0$ and $1$, and let $e(r)=1^r0$ for every natural number $r$, including $e(0)=0$. Membership $x\in C$ means that there exist natural numbers $n,k$, a finite Boolean list $B$, and a finite set $S\subseteq\{0,\ldots,n-1\}$ such that $x=e(n)e(k)B$, $|B|=n^2$, every diagonal entry $B_{un+u}$ for $u<n$ is false, $B_{un+v}=B_{vn+u}$ for every $u,v<n$, $k\leq |S|$, and $B_{un+v}$ is true for every distinct $u,v\in S$; concatenation is exact and indices start at zero. Equivalently, the underlying graph data are an arbitrary natural vertex count and Boolean list, adjacency requires both vertices to be below the count and the row-major list entry to be true, missing list entries default to false, and the language separately requires the list to have exactly the square of the vertex count entries and to describe a symmetric, loop-free graph. Thus the threshold $k$ is part of the input and ranges over all naturals, the selected vertices are distinct and in range, and the condition asks for at least $k$ selected vertices. A valid encoding has length $n^2+n+k+2$. Every valid simple graph is accepted at threshold $0$ using the empty set, including the graph with zero vertices and empty matrix, whose threshold-$0$ encoding is the two-bit string $00$; threshold $1$ is satisfied precisely when a valid graph has at least one vertex, and thresholds greater than $n$ are unsatisfied. Strings with missing unary delimiters, wrong matrix length, loops, asymmetry, or otherwise no such representation are outside $C$, including the empty string, even when a putative threshold is $0$. To specify the NP assertion, write $\mathcal N(L)$ for this property of a language $L\subseteq\{0,1\}^*$: there exist a total Boolean-valued function $V(x,w)$ on pairs of finite bit strings, natural witness-bound constants $a,b$, a machine $M$, and natural numbers $t,G,c,d$, such that $M$ is legal with $t$ tapes and alphabet size $G$, for every pair $x,w$ its execution from the initial configuration for $(x,w)$ after exactly $c(|x|+|w|+1)^d$ steps is in state $|M|$ and cell $1$ of tape $t-1$ contains the symbol for $V(x,w)$, every pair accepted by $V$ satisfies $|w|\leq a(|x|+1)^b$, and for every finite bit string $x$, $x\in L\iff\exists w\in\{0,1\}^*\;V(x,w)=\mathrm{true}$. The verdict and running-time conditions apply to every witness, including witnesses exceeding the certificate-length bound, which must be rejected; witnesses need not have exactly the bound length and need not be unique. The first conjunct of the theorem is $\mathcal N(C)$. Its second conjunct says that for every language $L\subseteq\{0,1\}^*$ satisfying $\mathcal N(L)$, there exist a total function $f:\{0,1\}^*\to\{0,1\}^*$, a machine $R$, and natural numbers $t_R,G_R,c_R,d_R$ such that $R$ is legal with $t_R$ tapes and alphabet size $G_R$ and, for every finite bit string $x$, if $T_x=c_R(|x|+1)^{d_R}$, then its execution from the initial configuration for $(x,\varepsilon)$ after exactly $T_x$ steps is in state $|R|$, its output as defined below is exactly $f(x)$, and $x\in L\iff f(x)\in C$. Here $\varepsilon$ is the empty bit string; the output is read from cell $1$ of tape $t_R-1$ at that final configuration, decoding consecutive bit symbols until either the first non-bit symbol or a maximum of $T_x+2$ cells have been inspected. No additional terminator condition after that maximum is imposed by the output definition. The function, machine, tape count, alphabet size, and polynomial constants may depend on $L$, but are fixed across all inputs to that reduction; the verifier and its constants are likewise fixed across all input/witness pairs for its language. In both conjuncts, a machine is a finite list of commands, with states numbered by natural numbers, initial state $0$, and halting state the length of that list. A command is a total function of the list of scanned natural-number symbols returning a next state and a list of write/move actions. Legality requires at least two tapes and an alphabet size at least four; on every scanned list of the stipulated tape count each command produces exactly that many actions and a next state at most the machine length, rewrites tape $0$ with its scanned symbol, and, whenever all scanned symbols are less than the alphabet size, writes only symbols below that size. Tapes have cells indexed by natural numbers; an action writes at the current head and then moves left, stays, or moves right, with left movement from cell $0$ remaining at $0$. One unit of time is one application of the transition operation, simultaneously applying the current command's actions to the tapes and setting its next state; at or above the machine length this operation leaves the configuration unchanged. Initially every head is at cell $0$, every tape has start symbol $1$ in cell $0$, tape $0$ holds the first bit string from cell $1$, tape $1$ holds the second bit string from cell $1$, all other tapes are empty after their start symbol, and all remaining cells contain blank symbol $0$; bit false is represented by symbol $2$ and bit true by symbol $3$. Only tape $0$ is required to be read-only, and tape $1$ may also be the verdict/output tape when there are exactly two tapes. The definitions impose no general requirement to preserve the initial start symbol on writable tapes. Being halted at the stated bound permits halting earlier, because halting configurations are fixed points. All polynomial coefficients and exponents are naturals, with zero permitted by their quantifiers, and bounds and correctness include empty inputs and empty witnesses. The statement supplies no particular verifier, certificate format, reducing function, numerical exponent, or coefficient; it does not assert uniqueness or injectivity of any of them, a reduction specifically from a satisfiability language, a WordRAM algorithm or WordRAM running-time bound, a simulation backend, a fixed-threshold completeness result, an algorithm that outputs a clique, or any separation of complexity classes. For a negative instance of $L$, reduction correctness requires only that $f(x)$ lie outside $C$, so it does not require the reduction to output a valid graph encoding on every input.