claimroutineinferred_dep

Polynomial space by sequential branches

Claim·§5.5 Constructing the forms and completing the proof·inside thmCounting zeros of sparse polynomials faster

Statement (paper)

Processing the branches one at a time and adding each branch's count to an integer accumulator ZZ initialized to 00 uses nOk,c(1)n^{O_{k,c}(1)} bits of space in total, since the construction and Proposition  use nOk,c(1)n^{O_{k,c}(1)} bits on each branch and, by disjointness of the branches, 0⩽Z⩽2n0\le Z\le 2^n throughout; the final value of ZZ is N(P)N(\mathcal P).

In plain English

Running the branches one at a time and adding each branch's count to an accumulator ZZ (starting at 00) needs only nOk,c(1)n^{O_{k,c}(1)} bits of space overall, and the final ZZ equals N(P)N(\mathcal P).

Why it's here

Each branch's construction and the counting routine of Proposition prop:count use polynomial space, and that space is reused from one branch to the next. Because the branches are disjoint, ZZ never exceeds 2n2^n and needs only nn-ish bits, so the exponentially many branches add no space. Summing the branch counts gives N(P)N(\mathcal P), as the branching claim shows.
Classified routine:
Standard space-reuse bookkeeping: running the disjoint branches sequentially with a single accumulator bounded by 2n2^n, relying on the per-branch polynomial-space bound of Proposition prop:count and the branch decomposition of the earlier branching claim.

Uses

propCost of counting solutions via factor evaluationclaimBranch on high-incidence variables

Used by

Nothing in the paper

Sources

PaperOpen
Section
§5.5 Constructing the forms and completing the proof
Page
—
Label
—
Line
main_full_version.tex:3199
Leannot aligned

Phase 2 aligns this node to a Lean declaration.

Friction

  • info
    inferred_dep
    outline: "Polynomial space by sequential branches" rests on claim-thm-overview-sparse-polynomials-1