claimroutine
Branch on high-incidence variables
Claim·§5.5 Constructing the forms and completing the proof·inside thmCounting zeros of sparse polynomials faster
Statement (paper)
Let , and , and let be the set of variables belonging to more than scopes. Then , so there are at most branches with ; each branch has the same number of free variables, after substituting the fixed bits neither the degree nor the number of monomials of any increases, and is the sum of the common-zero counts of the branches.
In plain English
Let be the set of variables appearing in more than scopes, where and . Then , so fixing gives at most branches, each with free variables and no increase in degree or monomial count, and the total count is the sum of the branch counts.
Why it's here
This step removes the variables that occur in too many scopes, at the price of at most branches, which fits within the target running time. Each branch then has bounded variable incidence, which the per-branch design needs. Because the branch counts add up to and the branches can be processed one after another, the result also supports the polynomial-space bound.
Classified routine:
A Markov-type averaging bound (at most M/b_0 \le n/\sqrt\lambda variables can have incidence above b_0) combined with standard branching on those variables, as in sparsification and other exponential-time algorithms; substituting constants cannot raise degree or monomial count, and the zero counts of the branches add up to the total.
Uses
Nothing else in the paper
Used by
Sources
PaperOpen
- Section
- §5.5 Constructing the forms and completing the proof
- Page
- —
- Label
—- Line
main_full_version.tex:3097
Leannot aligned
Phase 2 aligns this node to a Lean declaration.