claimroutineinferred_dep

Tree size via B-choice positions

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

Statement (paper)

For M⩾ΓM\ge\Gamma, the number of nodes of the tree is at most (Cn+1)∑a⩽⌊Γn/M⌋(Cna)⩽(Cn+1)2 2(Γn/M)log⁡2(4CM)(Cn+1)\sum_{a\le\lfloor\Gamma n/M\rfloor}\binom{Cn}{a}\le (Cn+1)^2\,2^{(\Gamma n/M)\log_2(4CM)}, since a node is determined by its depth and the positions at which its path chooses BB, and a path has depth at most CnCn and chooses BB at most Γn/M\Gamma n/M times.

In plain English

For M⩾ΓM\ge\Gamma, the sparsification tree has at most (Cn+1)∑a⩽⌊Γn/M⌋(Cna)(Cn+1)\sum_{a\le\lfloor\Gamma n/M\rfloor}\binom{Cn}{a} nodes, which is at most (Cn+1)2 2(Γn/M)log⁡2(4CM)(Cn+1)^2\,2^{(\Gamma n/M)\log_2(4CM)}.

Why it's here

Using the previous claim's bounds (depth at most CnCn, at most Γn/M\Gamma n/M B-choices per path), each node is pinned down by its depth and the set of positions where its path takes the BB-child, so counting these descriptions bounds the node count. The resulting exponent (Γn/M)log⁡2(4CM)(\Gamma n/M)\log_2(4CM) is what the next claim makes at most σn\sigma n by choosing MM appropriately.
Classified routine:
A standard counting argument from sparsification-lemma proofs (Impagliazzo–Paturi–Zane 2001 style): a node is determined by its depth and the positions of B-choices, and the binomial sum is bounded by the usual estimate on sums of binomial coefficients, applied to the bounds from the previous claim.

Uses

claimPath length and B-choice bounds

Used by

claimChoosing M keeps tree within 2^{sigma n}

Sources

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

Phase 2 aligns this node to a Lean declaration.

Friction

  • info
    inferred_dep
    outline: "Node count via path descriptions" rests on claim-lem-sparsify-2