LemmaStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedprecheck passaudited 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.

Logarithmic iteration reaches a constant unsatisfaction gap

Statement

Let $t$ be the fixed integer of One fixed-alphabet transformation doubles small gaps, let $α = \min (1 / 2, κ β c / \sqrt{t}) > 0$ be its cap, let $T : = T_{t}$ and let $C : = C_{E} \geq 1$ be the edge-growth constant of One fixed transformation has constant-factor growth. For every finite binary constraint graph $G_{0}$ over $Σ_{⋆}$ with $m = ∣ E (G_{0}) ∣ \geq 1$ edge records and $UNSAT (G_{0}) > 0$ , the iterates $G_{k} : = T^{k} (G_{0})$ at $k : = ⌈ \log_{2} m ⌉$ satisfy $UNSAT (G_{k}) \geq α, ∣ E (G_{k}) ∣ \leq C^{k} m = m^{O (1)} .$ If instead $UNSAT (G_{0}) = 0$ , then $UNSAT (G_{k}) = 0$ for every $k \geq 0$ : all iterates of a satisfiable graph are satisfiable.

Facts & Assumptions

Given: Fix the fixed integer $t$ , the map $T = T_{t}$ and the constants $α > 0$ and $C = C_{E} \geq 1$ .

[F1]

For every finite binary constraint graph $G$ over $Σ_{⋆}$ , $UNSAT (T (G)) \geq \min (2 UNSAT (G), α)$ . (One fixed-alphabet transformation doubles small gaps)

[F2]

$T$ is a deterministic map from finite $Σ_{⋆}$ -graphs to finite $Σ_{⋆}$ -graphs, the same transformation may be used in every round, and $α = \min (1 / 2, κ β c / \sqrt{t}) > 0$ . (One fixed-alphabet transformation doubles small gaps)

[F3]

For every finite $Σ_{⋆}$ -graph $G$ with $m = ∣ E (G) ∣$ edge records, $∣ E (T (G)) ∣ \leq C m$ , where $C = C_{E} \geq 1$ is a constant fixed before any input graph is given. (One fixed transformation has constant-factor growth)

[F4]

For every finite $Σ_{⋆}$ -graph $G$ with $val (G) = 1$ , $val (T (G)) = 1$ ; equivalently $UNSAT (G) = 0$ implies $UNSAT (T (G)) = 0$ . (One Dinur transformation preserves perfect satisfiability)

[F5]

For a labeling $σ$ the number ${val}_{σ} (G)$ is the fraction of ordinary edges satisfied when $E (G) \neq \emptyset$ , and $UNSAT (G) = \min_{σ} (1 - {val}_{σ} (G))$ ; hence for a graph with $m \geq 1$ edges and $UNSAT (G) > 0$ every labeling violates at least one edge, so $UNSAT (G) \geq 1 / m$ . (Constraint graph and labeling value)

Proof

Given: Use the fixed $T$ , $α$ and $C$ , and let $G_{0}$ be an arbitrary finite $Σ_{⋆}$ -graph with $m = ∣ E (G_{0}) ∣ \geq 1$ edge records and $UNSAT (G_{0}) > 0$ .

1.1F2given

Put $k : = ⌈ \log_{2} m ⌉$ and $u_{i} : = UNSAT (T^{i} (G_{0}))$ for $0 \leq i \leq k$ , where $T^{0}$ is the identity. By [F2] every iterate $T^{i} (G_{0})$ is again a finite $Σ_{⋆}$ -graph, so all $u_{i}$ are defined and [F1] and [F3] can be applied to each of them.

1.2F5givenalgebra

Since $m \geq 1$ and $u_{0} = UNSAT (G_{0}) > 0$ , every labeling of $G_{0}$ violates at least one of the $m$ edge records, so by [F5] $u_{0} \geq 1 / m$ .

2.1F1F2step 1.1algebra

We prove $u_{i} \geq \min (2^{i} u_{0}, α)$ for all $0 \leq i \leq k$ by induction on $i$ . For $i = 0$ this reads $u_{0} \geq \min (u_{0}, α)$ , which holds because $α > 0$ . For the induction step, assume $u_{i} \geq \min (2^{i} u_{0}, α)$ ; then [F1] applied to the finite $Σ_{⋆}$ -graph $T^{i} (G_{0})$ of step 1.1 gives $u_{i + 1} \geq \min (2 u_{i}, α) \geq \min (2 \min (2^{i} u_{0}, α), α) = \min (2^{i + 1} u_{0}, α)$ , using that $x \mapsto \min (2 x, α)$ is nondecreasing and $\min (2 a, 2 α, α) = \min (2 a, α)$ for $α > 0$ .

2.2F3step 1.1algebra

We prove $∣ E (T^{i} (G_{0})) ∣ \leq C^{i} m$ for all $0 \leq i \leq k$ by induction on $i$ : for $i = 0$ this is $∣ E (G_{0}) ∣ = m$ ; for the step, [F3] applied to the finite graph $T^{i} (G_{0})$ gives $∣ E (T^{i + 1} (G_{0})) ∣ \leq C ∣ E (T^{i} (G_{0})) ∣ \leq C^{i + 1} m$ . In particular $∣ E (G_{k}) ∣ \leq C^{k} m$ .

2.3F4F5step 1.1algebra

If $UNSAT (G_{0}) = 0$ , then equivalently $val (G_{0}) = 1$ by [F5], and [F4] applied to $G = T^{i} (G_{0})$ for $i = 0, \dots$ gives $val (T^{i + 1} (G_{0})) = 1$ whenever $val (T^{i} (G_{0})) = 1$ ; inductively $UNSAT (T^{i} (G_{0})) = 0$ for every $i \geq 0$ , so every iterate of a satisfiable graph is satisfiable.

3.1F2step 1.2step 2.1step 2.2step 2.3algebra∎

Since $k = ⌈ \log_{2} m ⌉$ gives $2^{k} \geq m$ , step 1.2 yields $2^{k} u_{0} \geq 2^{k} / m \geq 1$ , and step 2.1 yields $u_{k} \geq \min (2^{k} u_{0}, α) \geq \min (1, α) = α$ because $α \leq 1 / 2 < 1$ by [F2]. Moreover $k \leq \log_{2} m + 1$ and $C \geq 1$ , so $C^{k} \leq C^{\log_{2} m + 1} = C m^{\log_{2} C}$ and therefore $∣ E (G_{k}) ∣ \leq C^{k} m \leq C m^{1 + \log_{2} C} = m^{O (1)}$ by step 2.2. With step 2.3 this proves both clauses for the arbitrary graph $G_{0}$ .

Remarks

The point of the iteration is that the doubling lemma's cap $α$ is reached after only $⌈ \log_{2} m ⌉$ rounds once the initial unsatisfaction is positive, because a positive value on an $m$ -edge graph is at least $1 / m$ ; the growth lemma keeps the size polynomial, $m^{O (1)}$ , so no round is ever applied to an exponential-size object. The same fixed $t$ , the same $α$ and the same map $T$ are used in every round, and the satisfiable case is preserved separately by the completeness lemma. No choice principle is used: all iterates are determined by the fixed deterministic map $T$ .

Depends on

Used by

Constant-gap binary CSP is NP-hard Theorem

Dependency tree · two levels

9 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 Theorem 1.5 and the logarithmic-iteration paragraph, printed pp. 4–5 (standard reference, not scraped)
Sanjeev Arora and Boaz Barak, Computational Complexity: A Modern Approach, §18.5 (iteration of Lemma 18.28 log m times), printed p. 370 (standard reference, not scraped)