Alphabeta Math
TheoremStatement: AI-adaptedProof: AI-adaptedPipeline-generatedprecheck pass
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.

Constant-gap binary CSP is NP-hard

Statement

Assume the Axiom of Choice (The Axiom of Choice).

Let Σ⋆ be the fixed 66-symbol alphabet of One fixed-alphabet Dinur transformation, let T=Tt be the fixed transformation of One fixed-alphabet transformation doubles small gaps and let α=min⁡(1/2,κβc/t)>0 be its cap. Then GapCSP⁡(1,1−α) on explicit binary constraint graphs over Σ⋆, in the promise sense of Gap csp, is NP-hard under deterministic polynomial-time many-one promise reductions: for every language L∈NP there is a total function fL on instances, computable by a deterministic polynomial-time algorithm, such that fL(x) is an explicit binary constraint graph over Σ⋆ satisfying val⁡(fL(x))≥1for x∈L,val⁡(fL(x))≤1−αfor x∉L.

Facts & Assumptions

Given: Assume the Axiom of Choice and use the fixed alphabet Σ⋆, the fixed map T and the fixed cap α>0.

[F1]

For a three-CNF formula F with m clauses, each having exactly three literal occurrences, there is a polynomial-time binary constraint graph over the fixed alphabet Σ^={B(0),B(1)}⊔{T(a):a∈{0,1}3} with exactly 3m edges. Its value is one exactly when F is satisfiable. If F is unsatisfiable and m≥1, then UNSAT⁡(GF)≥13m. The zero-clause formula maps to an edgeless graph. (A three-CNF formula as a fixed-alphabet binary constraint graph)

[F2]

The language 3-SAT of satisfiable CNF formulas with exactly three literals per clause is NP-complete. (3-SAT is NP-complete)

[F3]

For every finite binary constraint graph G0 over Σ⋆ with m=∣E(G0)∣≥1 edge records and UNSAT⁡(G0)>0, the iterates Gk:=Tk(G0) at k:=⌈log⁡2m⌉ satisfy UNSAT⁡(Gk)≥α,∣E(Gk)∣≤Ckm=mO(1). (Logarithmic iteration reaches a constant unsatisfaction gap)

[F4]

If instead UNSAT⁡(G0)=0, then UNSAT⁡(Gk)=0 for every k≥0: all iterates of a satisfiable graph are satisfiable. (Logarithmic iteration reaches a constant unsatisfaction gap)

[F5]

The cap is α=min⁡(1/2,κβc/t)>0, a constant fixed before any input. (One fixed-alphabet transformation doubles small gaps)

[F6]

T is a deterministic map from finite Σ⋆-graphs to finite Σ⋆-graphs, so the same transformation can be used in every round. (One fixed-alphabet transformation doubles small gaps)

[F7]

GapCSP⁡(c,s) is the disjoint yes/no pair Y={G:val⁡(G)≥c},N={G:val⁡(G)≤s}, and for 0<ε≤1 the pair GapCSP⁡(1,1−ε) distinguishes satisfiability from UNSAT⁡(G)≥ε. (Gap csp)

[F8]

A polynomial-time many-one reduction from a language A to a language B is a total function f computable by a deterministic Turing machine in polynomial time with x∈A  ⟺  f(x)∈B for every instance x. (Polynomial-time many-one reductions)

[F9]

For a labeling σ the number val⁡σ(G) is the fraction of ordinary edges satisfied, and val⁡(G)=max⁡σval⁡σ(G), UNSAT⁡(G)=min⁡σ(1−val⁡σ(G)). (Constraint graph and labeling value)

[F10]

The transformation alphabet is the fixed alphabet of 66 symbols Σ⋆={B(0),B(1)}⊔{0,1}6. (One fixed-alphabet Dinur transformation)

[F11]

There are constants CE,CV≥1, fixed before any input, such that every finite Σ⋆-graph G with m=∣E(G)∣ edge records satisfies ∣E(T(G))∣≤CEm, ∣V(T(G))∣≤CVm, and T is deterministic and computable in time polynomial in the bit length of the explicit encoding of G. (One fixed transformation has constant-factor growth)

[A1]

The Axiom of Choice is assumed (The Axiom of Choice). It supplies the inherited premise of the current Dinur-transformation proof route through expander spectral theory and algebraic embedding extension.

Proof

Given: Assume the Axiom of Choice and use the fixed alphabet Σ⋆, the fixed map T and α>0, and let x be an arbitrary instance of a language L∈NP.

1.1A1F1F2F6F8F10givenconstruct

Under [A1], use the current Dinur-transformation suppliers [F3]–[F6], [F10] and [F11], whose proof route uses Choice through expander spectral theory and algebraic embedding extension. By [F2] and [F8] there is a deterministic polynomial-time total reduction g from L to 3-SAT, which we fix; put φ:=g(x), with m clauses, each of exactly three literal occurrences. By [F1] the formula φ has a polynomial-time computable graph Gφ over Σ^={B(0),B(1)}⊔{T(a):a∈{0,1}3} with exactly 3m edges, and by [F10] the transformation alphabet is Σ⋆={B(0),B(1)}⊔{0,1}6. Let f be the fixed injection f:Σ^→Σ⋆ with f(B(i))=B(i) and f(T(a))=(a,0,0,0), and let G^ be the graph with the same vertices, incidence slots and endpoint orders as Gφ and relations f(Re)={(f(a),f(b)):(a,b)∈Re}; then G^ is an explicit binary constraint graph over Σ⋆ with exactly 3m edges. Put K:=⌈log⁡2(3m)⌉ if m≥1, and define h(φ):=TK(G^) for m≥1 (a finite Σ⋆-graph by [F6]) while h(φ) is the edgeless graph over Σ⋆ for m=0.

2.1F1F9step 1.1algebra

For a labeling σ of G^, define σ0(v):=f−1(σ(v)) if σ(v)∈f(Σ^) and σ0(v):=B(0) otherwise. If an edge e is satisfied by σ in G^, then (σ(u),σ(v))∈f(Re), so both labels lie in f(Σ^) and (σ0(u),σ0(v))=(f−1σ(u),f−1σ(v))∈Re: the same edge is satisfied by σ0 in Gφ. Hence val⁡σ(G^)≤val⁡σ0(Gφ)≤val⁡(Gφ) for every σ by [F9], so val⁡(G^)≤val⁡(Gφ); conversely the labelings f∘τ of G^ for τ:V→Σ^ realize the same satisfied edges, so val⁡(G^)≥val⁡(Gφ). Thus val⁡(G^)=val⁡(Gφ) and UNSAT⁡(G^)=UNSAT⁡(Gφ).

2.2F1F8F11step 1.1algebra

For the size and time bound, each iterate multiplies the number of edge records by at most CE and has at most CV times the previous number of edge records vertices by [F11], so after i≤K=O(log⁡m) rounds ∣E(Ti(G^))∣≤CEi⋅3m and, for i≥1, ∣V(Ti(G^))∣≤CV∣E(Ti−1(G^))∣≤CVCEi−1⋅3m, both of size mO(1). Each of the K+1 applications of T runs in deterministic polynomial time in the bit length of its input by [F11], and that input has size mO(1) throughout, so the computation of h(φ) from φ is deterministic polynomial time; the relabeling Gφ↦G^ and the reduction g are also polynomial time.

3.1F1F4F9step 1.1step 2.1

Suppose x∈L, so φ∈3-SAT. If m=0, then h(φ) is edgeless, so val⁡(h(φ))=1 by [F9]. If m≥1, then val⁡(Gφ)=1 by [F1], hence val⁡(G^)=1 by step 2.1, and the zero-unsatisfaction clause [F4] of the iteration lemma applied to G0=G^ with ∣E(G^)∣=3m gives UNSAT⁡(h(φ))=0, that is, val⁡(h(φ))=1. In both cases val⁡(h(φ))≥1.

3.2F1F3F9step 1.1step 2.1

Suppose x∉L, so φ∉3-SAT is unsatisfiable; a formula with no clauses is satisfiable, so m≥1. By [F1], UNSAT⁡(Gφ)≥1/(3m)>0 and ∣E(Gφ)∣=3m≥1, and step 2.1 transfers both to G^, whose edge count is 3m. The positive-gap clause [F3] of the iteration lemma applied to G0=G^ with ∣E(G^)∣=3m and K=⌈log⁡2(3m)⌉ gives UNSAT⁡(h(φ))≥α, hence val⁡(h(φ))≤1−α by [F9].

4.1F2F5F7F8step 1.1step 2.2step 3.1step 3.2discharge-construct∎

The map fL:x↦h(g(x)) is total, deterministic and polynomial time by steps 1.1 and 2.2, and it sends instances of L to graphs of value at least 1 by step 3.1 and instances outside L to graphs of value at most 1−α by step 3.2. By [F7] the target pair is GapCSP⁡(1,1−α) with c=1 and s=1−α, and by [F8] this is a deterministic polynomial-time many-one promise reduction in the two-sided sense. Since L∈NP was arbitrary, GapCSP⁡(1,1−α) is NP-hard.

Remarks

The route is the classical one: 3-SAT is reduced to a fixed-alphabet binary constraint graph, the fixed transformation T is iterated logarithmically many times, and the Dinur transformation turns the 1/(3m) unsatisfaction gap of an unsatisfiable instance into the absolute gap α, while satisfiable instances stay satisfiable. The relabeling of the ten-symbol gadget alphabet into the 66-symbol alphabet Σ⋆ preserves value because a labeling that uses a symbol outside the image satisfies no edge incident to that vertex, so the clamped labeling satisfies at least as many edges. The reduction is deterministic and runs in polynomial time because the intermediate graphs have polynomially many edges and vertices. The Axiom of Choice premise is inherited from the current proof of the Dinur transformation: its expander spectral route reaches algebraic embedding extension and Zorn's lemma. This records the assumption spent by the supplied argument; it does not assert that the gap-CSP theorem intrinsically requires Choice.

Depends on

Used by

Dependency tree · two levels

23 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