claimroutineinferred_dep

Leaf occurrence bound and count partition

Claim·§A.3 The size of the tree·inside lemSparsification into bounded-occurrence k-CNF leaves

Statement (paper)

In every leaf of the tree, each variable occurs at most B=2∑j=0k−1Mj⩽4Mk−1=Ok([σ−1log⁡(2/σ)]k−1)B=2\sum_{j=0}^{k-1}M^j\le 4M^{k-1}=O_k\bigl(\bigl[\sigma^{-1}\log(2/\sigma)\bigr]^{k-1}\bigr) times. Moreover, each satisfying assignment of the input formula satisfies exactly one leaf formula, so the sum of the leaf counts equals the input count.

In plain English

In every leaf of the sparsification tree, each variable occurs at most B=2∑j=0k−1Mj⩽4Mk−1=Ok([σ−1log⁡(2/σ)]k−1)B=2\sum_{j=0}^{k-1}M^j\le 4M^{k-1}=O_k([\sigma^{-1}\log(2/\sigma)]^{k-1}) times. Also, each satisfying assignment of the input formula satisfies exactly one leaf formula, so the leaf counts sum to the input count.

Why it's here

The occurrence bound follows from the choice of M=Ok(σ−1log⁡(2/σ))M=O_k(\sigma^{-1}\log(2/\sigma)) in the previous claim, which turns the leaf degree bound into the stated BB. The count identity follows from the branching lemma's partition property, which makes children split the parent's satisfying assignments, so counting at the leaves loses nothing. Together these give the occurrence and counting guarantees of the main sparsification lemma.
Classified routine:
Direct bookkeeping consequence of the earlier choice of M (claim-lem-sparsify-4) and the partition property of the branching rule (lem-spar-branch), in the style of the Impagliazzo–Paturi–Zane sparsification lemma's leaf analysis.

Uses

claimChoosing M keeps tree within 2^{sigma n}lemSparsification branching rule is sound

Used by

Nothing in the paper

Sources

PaperOpen
Section
§A.3 The size of the tree
Page
—
Label
—
Line
main_full_version.tex:3855
Leannot aligned

Phase 2 aligns this node to a Lean declaration.

Friction

  • info
    inferred_dep
    outline: "Leaf occurrence bound and count partition" rests on claim-lem-sparsify-4
  • info
    inferred_dep
    outline: "Leaf occurrence bound and count partition" rests on lem:spar-branch