lemmaroutine

Marked clauses containing a set are few

Lemma·lem:spar-marked-degree·§A.2 Counting insertions

Statement (paper)

At every node, for

1\le i<j<k

and every literal set

S

of size

i

, fewer than

2\theta_{j-i}

marked clauses of width

j

that are still present contain

S

In plain English

At every node of the sparsification tree, for

1\le i<j<k

and any literal set

S

of size

i

, fewer than

2\theta_{j-i}

of the still-present marked clauses of width

j

contain

S

Why it's here

This is a degree bound on marked clauses: no small literal set lies in too many of them, with the threshold

\theta_{j-i}

depending only on how many extra literals the clause has beyond

S

. It is the invariant that lets the insertion counting (Lemma A.3) bound width-

j

insertions, and it supports the correctness of the sparsification lemma.

Classified routine:

This is the standard degree invariant from the sparsification lemma of Impagliazzo, Paturi and Zane (2001), where a sunflower-style flower reduction keeps the number of marked clauses containing any fixed literal set below a threshold. Here it is restated for this paper's own parameters θ.

Uses

Nothing else in the paper

Used by

lemSparsification into bounded-occurrence k-CNF leaveslemWidth-j insertions are linearly bounded

Sources

PaperOpen

Section: §A.2 Counting insertions
Page: —
Label: lem:spar-marked-degree
Line: main_full_version.tex:3740

Leannot aligned

Phase 2 aligns this node to a Lean declaration.