LemmaStatement: 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.

Cloud violations control distance to plurality labels

Statement

Let $G$ be a binary constraint graph over the fixed alphabet $Σ$ with $E (G) \neq \emptyset$ , let $G_{1}$ be its cloud graph as constructed by the degree-reduction map Degree reduction by expander incidence clouds, and let $τ$ be any labeling of the ports of $G_{1}$ with corresponding plurality decoding $σ = D τ$ . Write $S$ for the number of ports whose label differs from the decoded label $σ (v)$ of their original vertex $v$ , and let $U_{i n t}$ and $U_{e x t}$ count the equality edges inside clouds and the external edges that are violated by $τ$ . Then $U_{i n t} \geq \frac{7}{20} S, U_{G} \leq U_{e x t} + S,$ where $U_{G}$ is the number of ordinary edges of $G$ violated by the decoded labeling $σ$ .

Facts & Assumptions

Given: a binary constraint graph $G$ with $E (G) \neq \emptyset$ over the fixed alphabet, a labeling $τ$ of its cloud graph $G_{1}$ , the decoded labeling $σ = D τ$ , and the counts $S, U_{i n t}, U_{e x t}, U_{G}$ above.

[F1]

For any labeling of the cloud graph $G_{1}$ of a nonempty-edge constraint graph $G$ , decode each original vertex by its cloud's plurality label, using fixed tie breaking. Let $S$ count the ports disagreeing with that label, and let $U_{i n t}, U_{e x t}$ count violated internal equality and external edges. Then $U_{i n t} \geq (h_{0} / 2) S$ and $U_{G} \leq U_{e x t} + S$ with $h_{0} = 7 / 10$ , where $U_{G}$ is the decoded violation count in $G$ (Cloud plurality rounding).

[F2]

The cloud graph $G_{1}$ of the degree-reduction map has one port per incidence, a copy of $H_{r}$ with equality on every internal edge inside each cloud, one external edge per original edge joining the designated ports, and the same alphabet $Σ$ ; the fixed alphabet ordering is used both for the plurality choice of $D$ and for the tie-breaking in the published rounding bound (Degree reduction by expander incidence clouds).

Proof

technique · direct

1.1

The cloud graph and the decoding used here are the ones of [F2], with the same alphabet ordering and the same equality and external relations. Substituting $h_{0} = 7 / 10$ into the first inequality of [F1] gives $U_{i n t} \geq (7 / 20) S$ .

F1F2algebra

1.2

If some cloud contains no port at all, then it contributes neither ports nor edges to the counts; the second inequality of [F1] is a statement about all clouds simultaneously and covers this case. It gives $U_{G} \leq U_{e x t} + S$ , including $S = 0$ and including the case in which the decoded labeling fails an external edge whose two ports carry labels constant on their clouds.

F1F2

2.1

Both displayed inequalities therefore hold for every labeling $τ$ of the ports of $G_{1}$ , with the constants $7 / 20$ and $1$ read off from the published rounding argument; no additional hypothesis on $G$ beyond $E (G) \neq \emptyset$ is used.

step 1.1step 1.2∎

Remarks

This item is the page-local interface of the published rounding bound: its content is the published argument of Cloud plurality rounding, cited here with the page's notation, not re-derived. It lets Degree reduction preserves unsatisfaction quantitatively cite the cloud decoding estimate by ID without restating the construction.
The hypothesis $E (G) \neq \emptyset$ is inherited from the cloud construction: the edgeless input is handled by the separate empty-output convention of Degree reduction by expander incidence clouds, where there are no clouds and both sides of each inequality are zero.

Depends on

Used by

A cloud rounding calculation Example
Degree reduction preserves unsatisfaction quantitatively Theorem

Dependency tree · two levels

5 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, §4 proof of Lemma 4.1, pp. 13-14. (standard reference, not scraped)