TheoremStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedprecheck passjudge pass (gpt-6-sol)audited 2026-09-30

How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

The PCP theorem: NP equals PCP(log n, O(1))

Statement

$N P = PCP (\log n, O (1))$ in the shorthand of PCP classes with completeness and soundness: a language $K \subseteq {0, 1}^{*}$ belongs to NP if and only if there are a constant $s < 1$ , a bound $r (n) = O (\log n)$ and a constant bound $q$ with $K \in PCP (r, q; 1, s)$ over the binary proof alphabet. In particular every language in the class has a verifier with perfect completeness, soundness at most the fixed constant $s < 1$ , one fixed polynomial-length proof per input, $O (\log n)$ random bits and a constant number of nonadaptive bit queries.

Facts & Assumptions

Given: Use the shorthand convention of PCP classes with completeness and soundness and the fixed $GapCSP (1, 1 - α)$ promise problem of Constant-gap binary CSP is NP-hard.

[F1]

For every language $L \in N P$ there is a total function $f_{L}$ , computable by a deterministic polynomial-time algorithm, such that $f_{L} (x)$ is an explicit binary constraint graph over $Σ_{⋆}$ with $val (f_{L} (x)) \geq 1$ for $x \in L$ and $val (f_{L} (x)) \leq 1 - α$ for $x \notin L$ , where $α > 0$ is the fixed gap constant. (Constant-gap binary CSP is NP-hard)

[F2]

For every explicit binary constraint multigraph $G$ over a finite alphabet $Σ$ with $m \geq 1$ edges there is a nonadaptive verifier whose proof is a labeling $σ : V (G) \to Σ$ , which uses exactly $⌈ \log_{2} m ⌉$ random bits and reads at most two symbols, such that for every fixed labeling $\Pr [V^{σ} rejects] = \frac{m}{2^{⌈ \log_{2} m ⌉}} {UNSAT}_{σ} (G) \geq \frac{1}{2} {UNSAT}_{σ} (G);$ it has perfect completeness on satisfiable graphs, and if $UNSAT (G) \geq δ$ then every proof is rejected with probability at least $δ / 2$ . (Two-query PCPs and binary constraint graphs)

[F3]

If a binary proof convention is required, encoding each $Σ$ symbol by a fixed number of bits changes two symbol queries to a constant number of nonadaptive bit queries without changing the best acceptance probability. (Two-query PCPs and binary constraint graphs)

[F4]

A language $K$ belongs to $PCP (r, q; c, s)$ exactly when there are a verifier $V$ with randomness bound $r (n)$ and query bound $q (n)$ , a fixed finite proof alphabet, and a polynomial $p$ such that its addressable proof length $L_{V} (n)$ is at most $p (n)$ and: if $x \in K$ , there is one fixed proof $π$ with $\Pr [V^{π} (x) accepts] \geq c$ ; if $x \notin K$ , every fixed proof $π$ satisfies $\Pr [V^{π} (x) accepts] \leq s$ . (PCP classes with completeness and soundness)

[F5]

In the shorthand $PCP (\log n, O (1))$ the proof alphabet is ${0, 1}$ , the randomness is $O (\log n)$ , the number of bit queries is bounded by a constant, completeness is perfect ( $c = 1$ ), and soundness is at most some fixed constant $s < 1$ . (PCP classes with completeness and soundness)

[F6]

For a fixed input $x$ and a fixed proof $π$ , the acceptance probability is the proportion of the $2^{r (n)}$ coin strings on which $V^{π} (x)$ accepts, and the proof is not resampled when the verifier runs. (PCP verifier resources and deterministic proof strings)

[F7]

The class NP is the set of languages that admit a polynomial-time verifier with polynomially bounded certificates in the sense of Polynomial-time verifiers with polynomially bounded certificates. (The class NP via polynomial-time verifiers)

[F8]

A polynomial-time verifier with polynomially bounded certificates for $L$ consists of a relation $R$ whose paired language $L_{R} = {⟨ x, u ⟩ : (x, u) \in R}$ belongs to $P$ and a polynomial $p$ with $x \in L$ if and only if there is $u$ with $∣ u ∣ \leq p (∣ x ∣)$ and $(x, u) \in R$ . (Polynomial-time verifiers with polynomially bounded certificates)

[F9]

For a labeling $σ$ of a binary constraint graph $G$ with $E (G) \neq \emptyset$ , ${val}_{σ} (G)$ is the fraction of ordinary edges satisfied, and the definitions give $UNSAT (G) = 1 - val (G)$ with $val (G) = \max_{σ} {val}_{σ} (G)$ . (Constraint graph and labeling value)

[F10]

Between any two real numbers lies a rational (The rationals embed densely in the reals).

Proof

Given: Use the shorthand class convention of [F5] and the fixed gap problem [F1].

1.1F4F5F10givenconstruct

Suppose $K \in PCP (\log n, O (1))$ . By [F4] and [F5] there are a constant $s < 1$ , bounds $r (n) = O (\log n)$ and $q (n) = O (1)$ , a verifier $V$ with binary proof alphabet, and an integer-valued polynomial $p$ with $L_{V} (n) \leq p (n)$ such that on every input $x$ of length $n$ : if $x \in K$ some fixed proof is accepted with probability at least $1$ , and if $x \notin K$ every fixed proof is accepted with probability at most $s$ . Fix once and for all a rational constant $s^{'}$ with $s < s^{'} < 1$ ; [F10] supplies one, and the certificate machine can hardcode it without computing $s$ . Use the same query algorithm on proofs of length $p (n)$ ; its query locations remain in $[L_{V} (n)] \subseteq [p (n)]$ , so the added suffix is never read. Call this fixed-length interface $\hat{V}$ . Define the binary relation $R : = {(x, π) : ∣ π ∣ = p (∣ x ∣) and \Pr [{\hat{V}}^{π} (x) accepts] > s^{'}} .$ Thus every invocation in the relation has a valid fixed-length proof string.

1.2F1given

Suppose $L \in N P$ and fix the reduction $f_{L}$ of [F1]. For an input $x$ of length $n$ put $G_{x} : = f_{L} (x)$ and $M : = ∣ E (G_{x}) ∣$ ; then $x \in L$ implies $val (G_{x}) \geq 1$ and $x \notin L$ implies $val (G_{x}) \leq 1 - α$ , and $G_{x}$ together with its explicit encoding is computable in deterministic polynomial time in $n$ , so $M \leq p o l y (n)$ and the encoding length of $G_{x}$ is $p o l y (n)$ .

2.1F6step 1.1algebra

The paired language $L_{R} = {⟨ x, π ⟩ : (x, π) \in R}$ belongs to $P$ : a deterministic machine checks $∣ π ∣ = p (∣ x ∣)$ , enumerates the $2^{r (n)}$ coin strings of $\hat{V}$ on $x$ (there are $2^{O (\log n)} = p o l y (n)$ of them), simulates ${\hat{V}}^{π} (x)$ deterministically on each, counts the accepting runs, and compares the exact rational acceptance probability with the fixed rational $s^{'}$ by integer arithmetic.

2.2F1F9step 1.2

If $M = 0$ define the verifier $V_{0}$ that makes no queries and accepts on every coin string: it has perfect completeness, and it is used only when $val (G_{x}) = 1$ , which by [F9] is the value of an edgeless graph and by step 1.2 forces $x \in L$ (otherwise $val (G_{x}) \leq 1 - α < 1$ ), so its soundness clause is vacuous.

2.3F1F2F3step 1.2algebra

If $M \geq 1$ , apply [F2] to the graph $G_{x}$ over the alphabet $Σ_{⋆}$ and then the binary encoding of [F3] with a fixed $7$ -bit code for the $66$ symbols of $Σ_{⋆}$ . This yields a nonadaptive verifier $V_{x}$ whose proof is the concatenation of the $7$ -bit blocks of a vertex labelling, which uses exactly $⌈ \log_{2} M ⌉ = O (\log n)$ random bits by step 1.2, reads at most two $7$ -bit blocks, that is at most $14$ bit queries, and whose proof length is $7 ∣ V (G_{x}) ∣ = p o l y (n)$ because the explicit encoding of $G_{x}$ has polynomial length.

3.1F4F7F8step 1.1step 2.1algebra

By step 2.1 and [F7] it remains to verify the certificate condition of [F8] for $R$ . If $x \in K$ , pad its fixed $L_{V} (n)$ -bit completeness proof to length $p (n)$ ; $\hat{V}$ ignores the padding, so this proof has acceptance probability at least $1 > s^{'}$ and belongs to $R$ . Conversely, if $(x, π) \in R$ , the original verifier's queries are all in $[L_{V} (n)]$ , so the prefix of $π$ of length $L_{V} (n)$ is an original fixed proof with the same acceptance probability. If $x \notin K$ , soundness would bound that probability by $s < s^{'}$ , contrary to membership in $R$ . The certificate length is exactly $p (∣ x ∣)$ , hence at most $p (∣ x ∣)$ , so $K \in N P$ by [F7] and [F8].

3.2F2F3F9step 1.2step 2.2step 2.3

Completeness for $L$ : if $x \in L$ then $val (G_{x}) \geq 1$ . For $M = 0$ the verifier of step 2.2 accepts every coin string, so its one fixed proof is accepted with probability $1$ . For $M \geq 1$ , [F2] gives a labelling satisfying all $M$ edges, whose $7$ -bit encoding is a fixed binary proof accepted with probability $1$ by the verifier of step 2.3, the binary encoding of [F3] preserving the acceptance probability.

3.3F2F3F9step 1.2step 2.3algebra

Soundness for $L$ : if $x \notin L$ then step 1.2 and [F9] give $UNSAT (G_{x}) \geq α$ , so $M \geq 1$ and the verifier of step 2.3 is used. Fix any binary proof $π$ of the verifier's addressable length $7 ∣ V (G_{x}) ∣$ . Decode every consecutive $7$ -bit block by the fixed surjection $D : {0, 1}^{7} \to Σ_{⋆}$ from [F3]; this gives a full graph labeling $σ$ . Each real-edge index is accepted exactly when its edge relation is satisfied by $σ$ , so the number $S$ of accepted indices satisfies $S \leq M val (G_{x}) \leq M (1 - α)$ . The verifier accepts the $2^{⌈ \log_{2} M ⌉} - M$ surplus indices, so $\Pr [V_{x}^{π} (x) accepts] \leq \frac{2^{⌈ \log_{2} M ⌉} - M + M (1 - α)}{2^{⌈ \log_{2} M ⌉}} \leq 1 - \frac{α}{2},$ because $M / 2^{⌈ \log_{2} M ⌉} \geq 1 / 2$ . Hence every fixed binary proof is accepted with probability at most $1 - α / 2 < 1$ .

4.1F4F5step 1.2step 2.2step 2.3step 3.2step 3.3

Steps 2.2, 2.3, 3.2 and 3.3 exhibit, for the arbitrary language $L \in N P$ , a uniform deterministic polynomial-time verifier computing $G_{x}$ and then running the described test, with $O (\log n)$ random bits, a constant number of nonadaptive bit queries, binary proof alphabet, polynomial addressable proof length, perfect completeness and soundness at most $s : = 1 - α / 2 < 1$ . By [F4] and [F5], $L \in PCP (r, q; 1, s)$ for $r (n) = O (\log n)$ and constant $q$ , hence $L \in PCP (\log n, O (1))$ ; $L$ was arbitrary, so $N P \subseteq PCP (\log n, O (1))$ .

5.1step 3.1step 4.1∎

Step 3.1 gives $PCP (\log n, O (1)) \subseteq N P$ and step 4.1 gives the reverse inclusion, so $N P = PCP (\log n, O (1))$ in the shorthand sense, with perfect completeness, constant soundness below one, one fixed polynomial-length proof per input, $O (\log n)$ random bits and a constant number of nonadaptive bit queries.

Remarks

The two inclusions use different faces of the same gap: soundness of the fixed-alphabet gap problem supplies the constant rejection probability $α / 2$ for a randomly sampled constraint, while the enumeration of the $2^{O (\log n)}$ coin strings turns any PCP verifier into a polynomial-time certificate checker. Both quantifications are over one fixed proof: the verifier never resamples the proof, and the NP machine guesses it once. The gap problem is the one produced by the Dinur transformation of Constant-gap binary CSP is NP-hard, so no additional hardness assumption enters, and no choice principle is used: the reduction, the sampled edge and the guessed certificate are all explicit finite objects.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

27 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources

Irit Dinur, The PCP Theorem by Gap Amplification, §1.3 Theorems 1.1, 1.2 and 1.5, printed pp. 2–5 (standard reference, not scraped)
Sanjeev Arora and Boaz Barak, Computational Complexity: A Modern Approach, §18.1–18.2 (PCP and NP) and §18.5 (proof of the PCP theorem), printed pp. 350–379 (standard reference, not scraped)