TheoremStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedprecheck passaudited 2026-09-27

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.

A complete uniform graph gap-amplification step

Statement

Fix a finite alphabet $Σ$ with $∣ Σ ∣ \geq 2$ and put $D : = 387$ , $K : = 20 / 7$ , and let $β_{0}, t_{0}$ be the constants of Powering amplifies a small unsatisfaction gap for $d = D$ , this $Σ$ and $α_{0} : = ρ_{2} < 1$ , the spectral bound of Constraint expander overlay. For every integer $t \geq t_{0}$ there is a complete uniform gap-preserving reduction $R_{t}$ in the sense of Complete uniform gap-preserving CSP reductions, defined on binary constraint graphs over $Σ$ of arbitrary degree, with

$R_{t} (G) : = (R_{\deg} (G))_{t}$ , where $R_{\deg}$ is the degree-reduction map of Degree reduction by expander incidence clouds and $(\cdot)_{t}$ is the local-view powering of Constraint graph powering with local-view labels;
output alphabet $Σ_{t} = Σ^{P_{R}}$ of size $∣ Σ_{t} ∣ \leq ∣ Σ ∣^{D^{O (t)}}$ , output degree bound $d_{t} : = 2 (2 D)^{2 t + 1} = D^{O (t)}$ , and blowup $C_{t} : = D \cdot (2 D)^{2 t + 1} = D^{O (t)}$ ;
gap map $g_{t} (ε) = β \sqrt{t} \min (ε, c / t)$ with $c : = D K = 7740 / 7$ and $β : = β_{0} / (D K) > 0$ , so $UNSAT (R_{t} (G)) \geq β \sqrt{t} \min (UNSAT (G), c / t)$ and hence $UNSAT (G) \geq ε$ implies $UNSAT (R_{t} (G)) \geq β \sqrt{t} \min (ε, c / t)$ ;
perfect completeness: $val (G) = 1$ implies $val (R_{t} (G)) = 1$ , and edgeless inputs are mapped to edgeless outputs;

and $R_{t}$ is deterministic and runs in time polynomial in the bit length of the explicit encoding of $G$ . The constants $β, c, t_{0}$ and the parameters $Σ_{t}, d_{t}, C_{t}$ depend only on $∣ Σ ∣$ and $t$ , never on $∣ V (G) ∣$ or $∣ E (G) ∣$ . This is a single powering step, not the fixed-alphabet PCP iteration: the alphabet grows with $t$ , and no claim is made here about reducing it.

Facts & Assumptions

Given: a finite alphabet $Σ$ with $∣ Σ ∣ \geq 2$ , integers $t \geq t_{0}$ and $D = 387$ , $K = 20 / 7$ , and the constants $β_{0}, t_{0}$ of Powering amplifies a small unsatisfaction gap for $d = D$ , $Σ$ and $α_{0} = ρ_{2}$ .

[F1]

$R_{\deg}$ is a complete uniform gap-preserving reduction for the fixed input alphabet $Σ$ and arbitrary input degrees, with output alphabet $Σ$ , output degree bound $D$ , blowup $D$ , gap map $g_{\deg} (ε) = ε / (D K)$ , and polynomial running time; on inputs with $E (G) \neq \emptyset$ its output is $D$ -regular with $2 ∣ E (G) ∣$ vertices and $D ∣ E (G) ∣$ ordinary edges over $Σ$ and normalized second eigenvalue bound at most $ρ_{2} < 1$ (Degree reduction preserves unsatisfaction quantitatively, Constraint expander overlay, Degree reduction by expander incidence clouds).

[F2]

For a $d$ -regular graph $G$ with $n$ vertices, the powered graph $G_{t}$ has vertex set $V (G)$ , two paired incidence slots for each of the $n (2 d)^{2 t + 1}$ pairs (start vertex, pattern), degree $2 (2 d)^{2 t + 1}$ , and $n (2 d)^{2 t + 1}$ ordinary edges; its normalized adjacency is the length- $(2 t + 1)$ lazy-walk transition matrix, and its view alphabet is $Σ_{t} = Σ^{P_{R}}$ with $R = t + ⌈ \sqrt{t} ⌉$ . Explicit relation tables are computable by enumerating patterns and tables, so $G_{t}$ is produced in time polynomial in its explicit encoding length (Constraint graph powering with local-view labels).

[F3]

If $val (G_{2}) = 1$ then $val ((G_{2})_{t}) = 1$ (Powering preserves perfect satisfiability).

[F4]

For every labeling $φ$ of $(G_{2})_{t}$ , ${UNSAT}_{φ} ((G_{2})_{t}) \geq β_{0} \sqrt{t} \min (UNSAT (G_{2}), 1 / t)$ whenever $t \geq t_{0}$ and $G_{2}$ is $D$ -regular over $Σ$ with normalized second eigenvalue bound at most $ρ_{2}$ and at least one edge (Powering amplifies a small unsatisfaction gap).

[F5]

A complete uniform gap-preserving reduction has arity two throughout, maps edgeless inputs to edgeless outputs, obeys $∣ E (R (G)) ∣ \leq C ∣ E (G) ∣$ and $∣ V (R (G)) ∣ \leq C ∣ E (G) ∣$ on nonempty inputs, and its parameters depend only on the fixed input parameters and on the reduction itself (Complete uniform gap-preserving CSP reductions).

Proof

technique · direct

1.1

If $G$ is $D$ -regular over $Σ$ with at least one edge, [F2] gives a powered graph on $∣ V (G) ∣$ vertices, degree $d_{t} = 2 (2 D)^{2 t + 1}$ , and $∣ E (G_{t}) ∣ = ∣ V (G) ∣ (2 D)^{2 t + 1} = 2 (2 D)^{2 t + 1} ∣ E (G) ∣ / D \leq C_{t} ∣ E (G) ∣$ , since $D \geq 2$ . Also $∣ V (G_{t}) ∣ = ∣ V (G) ∣ = 2 ∣ E (G) ∣ / D \leq C_{t} ∣ E (G) ∣$ . Completeness is [F3], the gap bound is [F4], and the construction is explicit and polynomial for fixed $D, t, ∣ Σ ∣$ by [F2]. This establishes the powering facts on the regular intermediate graphs used below.

F2F3F4algebra

2.1

The gap map of the composite is $g (ε) = g_{t} (g_{\deg} (ε)) = β_{0} \sqrt{t} \min (ε / (D K), 1 / t)$ with $g_{\deg} (ε) = ε / (D K)$ as in [F1]; writing $\min (ε / (D K), 1 / t) = (1 / (D K)) \min (ε, D K / t)$ gives $g (ε) = β \sqrt{t} \min (ε, c / t)$ with $β = β_{0} / (D K)$ and $c = D K > 0$ .

F1step 1.1algebra

3.1

Define $R_{t} (G) = (R_{\deg} (G))_{t}$ . If $E (G) \neq \emptyset$ , [F1] gives a $D$ -regular intermediate graph with $2 ∣ E (G) ∣$ vertices, so [F2] gives $∣ V (R_{t} (G)) ∣ = 2 ∣ E (G) ∣$ , degree $d_{t}$ , and $∣ E (R_{t} (G)) ∣ = 2 ∣ E (G) ∣ (2 D)^{2 t + 1} \leq C_{t} ∣ E (G) ∣$ because $D \geq 2$ ; the vertex bound follows as well. Completeness follows by [F1] and [F3]. Applying [F1] and then [F4] gives the gap map of step 2.1. If $E (G) = \emptyset$ , the first map returns the empty graph and the powered output is empty, so the empty-input, completeness, and gap-at-zero clauses hold. The construction is deterministic and polynomial time: [F1] computes the intermediate graph in polynomial time and its size is $O (∣ E (G) ∣)$ for fixed $D, ∣ Σ ∣$ , after which [F2] enumerates a fixed number of patterns per vertex and writes fixed-size tables. Thus $R_{t}$ satisfies the clauses of [F5] directly, without applying a composition theorem whose second-stage domain is larger than the regular range used here.

F1F2F3F4F5step 2.1algebra

4.1

The alphabet size obeys $∣ Σ_{t} ∣ = ∣ Σ ∣^{(2 D)^{R}}$ with $R = t + ⌈ \sqrt{t} ⌉$ , which is at most $∣ Σ ∣^{D^{O (t)}}$ ; the degree $2 (2 D)^{2 t + 1}$ and blowup $D (2 D)^{2 t + 1}$ are both $D^{O (t)}$ ; and the gap inequality for inputs with $UNSAT (G) \geq ε$ follows from the gap map of step 2.1 and the monotonicity of $ε \mapsto \min (ε, c / t)$ . This proves every clause of the statement, with the stated dependence of all constants on $∣ Σ ∣$ and $t$ only.

F1F2step 1.1step 2.1step 3.1algebra∎

Remarks

The loss factor of the page is here. The factor $D K = 7740 / 7$ of Degree reduction preserves unsatisfaction quantitatively is absorbed into $β$ and into the saturation threshold $c$ , exactly as the promised claim allows; no other quantity of the composite depends on the internal constant $129$ of the cloud construction. The saturation threshold $c / t$ is inherited from the $\min (ε, 1 / t)$ of the powering lemma, scaled by the degree-reduction loss.
Not yet a PCP reduction. The output alphabet $Σ_{t}$ grows like $∣ Σ ∣^{D^{O (t)}}$ , and the output degree $d_{t}$ also grows with $t$ ; both are constants for fixed $t$ , which is what the statement needs, but a fixed-alphabet PCP requires the alphabet-reduction step that is owned by the following page. The obligation is recorded in the coverage record of this page rather than discharged here.
Determinism. The reduction enumerates all patterns and all relation tables instead of sampling them, so no random choices and no choice principle are used; the graph family $H_{r}$ inside $R_{\deg}$ is the explicit one supplied by the published expander construction. The pair $Σ_{t}$ is fixed by listing the patterns in a fixed order, which also fixes the tie-breaking order used by the plurality decoding of Plurality decoding of powered local views.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

20 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 Lemmas 1.6-1.7 and §1.2, printed pp. 5-7. (standard reference, not scraped)
Arora and Barak, Computational Complexity: A Modern Approach, §18.5.1 Lemma 18.29 (graph gap amplification), printed pp. 371-373. (standard reference, not scraped)