lemmaroutine

Width-j insertions are linearly bounded

Lemma·lem:spar-insertion-bound·§A.2 Counting insertions

Statement (paper)

Along any path or path prefix, the total number TjT_j of width-jj insertions satisfies Tj⩽4(3M)j−1nT_j\le4(3M)^{j-1}n for 1⩽j<k1\le j<k.

In plain English

Along any root-to-node path or path prefix in the sparsification tree, the total number TjT_j of width-jj clause insertions is at most 4(3M)j−1n4(3M)^{j-1}n, for each 1⩽j<k1\le j<k.

Why it's here

This turns the local marked-degree bound (Lemma A.2) and the branching bookkeeping (Lemma A.1) into a global count of insertions per width, with a bound linear in nn. Summing these bounds over jj gives the path-length bound CnCn and the cap on BB-choices that the main sparsification lemma needs.
Classified routine:
Standard counting step in the Impagliazzo–Paturi–Zane sparsification lemma analysis (Impagliazzo, Paturi, Zane 2001), combining the earlier marked-degree bound and branching bookkeeping into a linear-in-n bound on insertions per width by induction on j.

Uses

lemMarked clauses containing a set are fewlemSparsification branching rule is sound

Used by

lemSparsification into bounded-occurrence k-CNF leavesclaimPath length and B-choice bounds

Sources

PaperOpen
Section
§A.2 Counting insertions
Page
—
Label
lem:spar-insertion-bound
Line
main_full_version.tex:3771
Leannot aligned

Phase 2 aligns this node to a Lean declaration.