LemmaStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedprecheck passjudge pass (gpt-6-sol)audited 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.

Complete linear-blowup reductions compose

Statement

Let $R_{1}$ be a complete uniform gap-preserving reduction with output alphabet $Σ_{1}$ , output degree bound $d_{1}$ , blowup $C_{1}$ and gap map $g_{1}$ , defined for input alphabets of size $s$ and input degrees at most $d$ . Assume also that $R_{1} (G)$ has at least one edge whenever $G$ has at least one edge. Let $R_{2}$ be a complete uniform gap-preserving reduction with output alphabet $Σ_{2}$ , output degree bound $d_{2}$ , blowup $C_{2}$ and gap map $g_{2}$ , defined for input alphabets of size at least $∣ Σ_{1} ∣$ and input degrees at most $d_{1}$ . Then the composition $R_{2} \circ R_{1}$ , which on input $G$ first computes $R_{1} (G)$ and then $R_{2} (R_{1} (G))$ , is a complete uniform gap-preserving reduction for input alphabets of size $s$ and input degrees at most $d$ , with output alphabet $Σ_{2}$ , output degree bound $d_{2}$ , blowup $C_{1} C_{2}$ , gap map $g_{2} \circ g_{1}$ , and running time polynomial in the bit length of the explicit input encoding of $G$ .

Facts & Assumptions

Given: complete uniform gap-preserving reductions $R_{1}, R_{2}$ with the parameters and compatibility hypotheses in the statement, including the assumption that $R_{1}$ does not erase all edges of a nonempty input, and an input graph $G$ over an alphabet of size $s$ with all vertex degrees at most $d$ .

[F1]

A complete uniform gap-preserving reduction $R$ with output alphabet $Σ^{'}$ , output degree bound $d^{'}$ , blowup $C$ and gap map $g$ satisfies: $∣ E (R (G)) ∣ \leq C ∣ E (G) ∣$ and $∣ V (R (G)) ∣ \leq C ∣ E (G) ∣$ whenever $E (G) \neq \emptyset$ ; an edgeless input is mapped to an edgeless output; $UNSAT (G) = 0$ implies $UNSAT (R (G)) = 0$ ; $UNSAT (R (G)) \geq g (UNSAT (G))$ with $g$ nondecreasing, $g (0) = 0$ and $g (ε) > 0$ for $ε > 0$ ; all degrees of $R (G)$ are at most $d^{'}$ , the arity remains two, and $R$ runs in polynomial time in the encoding length of its input (Complete uniform gap-preserving CSP reductions).

[A2]

The additional edge-preservation condition in the statement ensures that if $G$ has an edge, then $R_{1} (G)$ is a nonempty input for the size clauses of $R_{2}$ .

Proof

technique · direct

1.1

If $E (G) = \emptyset$ then $R_{1} (G)$ is edgeless by [F1], hence so is $R_{2} (R_{1} (G))$ , as required for an edgeless input. If $E (G) \neq \emptyset$ , [A2] gives $E (R_{1} (G)) \neq \emptyset$ , so [F1] applied twice yields $∣ E (R_{2} (R_{1} (G))) ∣ \leq C_{2} ∣ E (R_{1} (G)) ∣ \leq C_{1} C_{2} ∣ E (G) ∣$ and $∣ V (R_{2} (R_{1} (G))) ∣ \leq C_{2} ∣ E (R_{1} (G)) ∣ \leq C_{1} C_{2} ∣ E (G) ∣$ ; all degrees of $R_{1} (G)$ are at most $d_{1}$ and its alphabet is $Σ_{1}$ , so $R_{2}$ is applicable to it.

F1A2algebra

1.2

If $UNSAT (G) = 0$ then two applications of the completeness clause of [F1] give $UNSAT (R_{1} (G)) = 0$ and then $UNSAT (R_{2} (R_{1} (G))) = 0$ , so the composite is complete.

1.3

For the gap map, two applications of the gap clause of [F1] give $UNSAT (R_{2} (R_{1} (G))) \geq g_{2} (UNSAT (R_{1} (G))) \geq g_{2} (g_{1} (UNSAT (G)))$ , the second inequality because $g_{2}$ is nondecreasing and $UNSAT (R_{1} (G)) \geq g_{1} (UNSAT (G))$ ; the composition $g_{2} \circ g_{1}$ is nondecreasing, vanishes at $0$ and is positive on $(0, 1]$ , so it is an admissible gap map.

F1algebra

2.1

For uniformity, the encoding length of $R_{1} (G)$ is bounded by a polynomial in the encoding length of $G$ : the alphabet $Σ_{1}$ is fixed, all degrees are at most $d_{1}$ , and the vertex and edge counts obey the linear bounds of step 1.1; the running time of $R_{1}$ on $G$ and of $R_{2}$ on $R_{1} (G)$ is polynomial in the respective encoding lengths by [F1], so with the shape, completeness and gap clauses of step 1.1, step 1.2 and step 1.3 the composite runs in polynomial time in the encoding length of $G$ and is a complete uniform gap-preserving reduction with output alphabet $Σ_{2}$ , output degree bound $d_{2}$ , blowup $C_{1} C_{2}$ and gap map $g_{2} \circ g_{1}$ .

F1step 1.1step 1.2step 1.3algebra∎

Remarks

The compatibility hypotheses are not cosmetic: $R_{2}$ is applied to a graph whose alphabet is $Σ_{1}$ and whose degrees are bounded by $d_{1}$ , and step 1.1 is exactly where those two fixed parameters, together with the edge bound, keep the intermediate explicit encoding polynomially short. Without a bound on the intermediate encoding length the composition of two polynomial-time algorithms need not be polynomial time in the original input length.
The edge blowup multiplies and the gap maps compose in the order the reductions are applied; no constant is lost. Later items of this page use the lemma with $R_{1}$ the degree-reduction map and $R_{2}$ the powering map.

Depends on

Complete uniform gap-preserving CSP reductions

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

3 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 and §3: the composed reduction (prep)ᵗ∘P, pp. 6-7 and 11-12. (standard reference, not scraped)
Arora and Barak, Computational Complexity: A Modern Approach, §18.5 Definition 18.27 (complete linear-blowup reductions). (standard reference, not scraped)