TheoremStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedprecheck passjudge pass (gpt-6.1-sol)audited 2026-10-02

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.

Maximum independent set has no PTAS unless P=NP

Statement

Assume the Axiom of Choice for the currently published PCP supplier proof route. A polynomial-time approximation scheme for maximum independent set on finite simple graphs implies $P = N P$ . On the graphs $G_{x}$ from the two gap reductions, $α (G_{x}) = M$ when $x$ is a yes instance and $α (G_{x}) \leq (1 - δ) M$ when $x$ is a no instance, for the same fixed $δ > 0$ .

Facts & Assumptions

Given: A language $L \in N P$ , a PTAS $A = (A_{ϵ})$ for the maximum independent set problem on finite simple graphs, and the two gap reductions below.

[F1]

Under the Axiom of Choice for its published proof route, the PCP verifier gives, for each input $x$ , a 3-CNF formula $F_{x}$ with $M \geq 1$ clauses and a fixed $δ > 0$ such that $x \in L$ implies ${OPT}_{M a x 3 S A T} (F_{x}) = M$ and $x \notin L$ implies ${OPT}_{M a x 3 S A T} (F_{x}) \leq (1 - δ) M$ . (A constant-query PCP verifier yields constant-gap Max-3SAT)

[F2]

The clause-literal consistency graph $G$ of a 3-CNF formula with $m$ clauses of three literal occurrences is a simple graph with $3 m$ vertices, computable in polynomial time, with $α (G) = {OPT}_{M a x 3 S A T} (F)$ ; for $m \geq 1$ the gap promise $m$ versus $(1 - δ) m$ transfers with unchanged $δ$ and positive scale $m$ , and any independent set of size $k$ decodes in polynomial time to an assignment satisfying at least $k$ clauses. (Clause-literal consistency graph preserves the Max-3SAT optimum, Gap promise problems and gap-preserving reductions)

[F3]

A subset of the vertex set of a finite simple graph is independent when no two of its vertices are adjacent, and $α (G)$ denotes the largest size of an independent set. (Clique, independent set, and vertex cover decision problems)

[F4]

A PTAS for a maximization problem is a family $(A_{ϵ})_{0 < ϵ < 1}$ such that for every fixed $ϵ$ the algorithm runs in polynomial time in the input length and returns a feasible solution of value at least $(1 - ϵ)$ times the optimum, in the value-inequality sense. (PTAS, FPTAS and APX)

[F5]

$P$ is the class of languages decided by some deterministic Turing machine in polynomial time, and every language in $P$ belongs to $N P$ , so $P \subseteq N P$ . (The class P, $P \subseteq N P \cap c o N P$ , The class NP via polynomial-time verifiers)

[F6]

$C$ is NP-hard when every language $L \in N P$ reduces to it in polynomial time. (NP-hard and NP-complete languages)

[F7]

The Axiom of Choice states that every family of nonempty sets has a choice function; it is assumed here solely through the published PCP supplier route used by [F1]. (The Axiom of Choice)

Proof

technique · direct

1.1F1F2F3F4F7givenconstruct

Fix $L \in N P$ and the reduction of [F1], which supplies the fixed constant $δ > 0$ and, for each input $x$ , the formula $F_{x}$ with $M \geq 1$ clauses; for each $x$ apply the polynomial-time construction of [F2] to obtain the finite simple graph $G_{x}$ with $3 M$ vertices and $α (G_{x}) = {OPT}_{M a x 3 S A T} (F_{x})$ , whose scale is the number $M$ of clause clusters. Assume the PTAS $A = (A_{ϵ})$ of [F4] and fix a rational $ϵ$ with $0 < ϵ < δ$ , for instance $ϵ = δ / 2$ . The PCP supplier route is used under the Axiom of Choice hypothesis of [F7].

2.1F1F2step 1.1algebra

By [F1] and the exact optimum equality of [F2], the graphs $G_{x}$ satisfy $α (G_{x}) = {OPT}_{M a x 3 S A T} (F_{x}) = M$ when $x \in L$ , and $α (G_{x}) = {OPT}_{M a x 3 S A T} (F_{x}) \leq (1 - δ) M$ when $x \notin L$ ; the scale $M$ is positive and unchanged, so the same fixed $δ > 0$ separates the two cases.

3.1F2F3F4step 2.1construct

Define the decision procedure: on input $x$ , construct $G_{x}$ , run the fixed algorithm $A_{ϵ}$ on $G_{x}$ to obtain an independent set $I$ , let $s = ∣ I ∣$ , and accept $x$ exactly when $s > (1 - δ) M$ . The graph construction is polynomial by [F2], the algorithm $A_{ϵ}$ is polynomial time for the fixed $ϵ$ by [F4], and the returned set is independent of size $s$ ; by the PTAS guarantee the value satisfies $s \geq (1 - ϵ) α (G_{x})$ .

4.1F4step 2.1step 3.1algebra

If $x \in L$ , then $α (G_{x}) = M$ by step 2.1, so $s \geq (1 - ϵ) M > (1 - δ) M$ because $ϵ < δ$ ; hence the procedure accepts $x$ .

4.2F3step 2.1step 3.1algebra

If $x \notin L$ , then $α (G_{x}) \leq (1 - δ) M$ by step 2.1, and $s \leq α (G_{x})$ because $s$ is the size of an independent set; hence $s \leq (1 - δ) M$ and the procedure rejects $x$ .

5.1F5F6step 4.1step 4.2algebra∎

Steps 4.1 and 4.2 show that the deterministic polynomial-time procedure accepts exactly the inputs of $L$ , so $L \in P$ ; since $L \in N P$ was arbitrary (the quantifier in [F6]), $N P \subseteq P$ , and $P \subseteq N P$ by [F5], so $P = N P$ . Therefore a PTAS for maximum independent set implies $P = N P$ , and on the graphs $G_{x}$ one has $α (G_{x}) = M$ for yes instances and $α (G_{x}) \leq (1 - δ) M$ for no instances with the same fixed $δ > 0$ .

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

24 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

Arora and Barak, Computational Complexity: A Modern Approach, §18.2.5 Lemma 18.16 and Remark 18.17, printed pp. 359–361 (standard reference, not scraped)