lemmaroutine

Sparsification branching rule is sound

Lemma·lem:spar-branch·§A.1 The branching rule

Statement (paper)

The children in partition the satisfying assignments of their parent. Every new clause has width less than cc. The AA-child inserts one new clause, and the BB-child inserts at least θj\theta_j new clauses of width jj. All newly inserted clauses survive the immediate normalization. Every old clause removed in either child contains a newly inserted strict subset.

In plain English

The branching rule's children partition the parent's satisfying assignments, and every new clause has width less than cc. The AA-child inserts one new clause, the BB-child inserts at least θj\theta_j new clauses of width jj, all new clauses survive immediate normalization, and every removed old clause contains a newly inserted strict subset.

Why it's here

This lemma is the local correctness and bookkeeping step for the sparsification tree: the partition property keeps satisfying assignments exactly accounted for, while the insertion counts and subset property let later lemmas bound path length, width-jj insertions, and variable occurrences at leaves. It is used by the main sparsification lemma and by the insertion-bound and path-length claims.
Classified routine:
This is the local soundness and bookkeeping check for the flower/sunflower branching rule of the Impagliazzo–Paturi–Zane sparsification lemma (2001): one child inserts the heart, the other inserts the petals, followed by subsumption normalization. Verifying it is a direct check.

Uses

Nothing else in the paper

Used by

lemSparsification into bounded-occurrence k-CNF leaveslemWidth-j insertions are linearly boundedclaimPath length and B-choice boundsclaimLeaf occurrence bound and count partition

Sources

PaperOpen
Section
§A.1 The branching rule
Page
—
Label
lem:spar-branch
Line
main_full_version.tex:3695
Leannot aligned

Phase 2 aligns this node to a Lean declaration.