propositionroutineinferred_dep

Cost of counting solutions via factor evaluation

Proposition·prop:count·§5.4 Cost of evaluating the factors

Statement (paper)

Let a list of degree-at-most-

k

polynomial equations on

n

variables and a design satisfying Definition for their factors be given. Let

S\ge1

bound the total length of the monomial lists and factor scopes, and use any

\ell

with

2^\ell>2^n

. With

d_H

from and

q,J

from ,

N(\mathcal P)

can be computed deterministically in

\poly(n,m_{\mathrm{test}},\ell,D,Q,R,J,r,k,S)\, C_q(2D+1)^{2\tau n}2^{2n/r}

bit operations and

\poly(n,m_{\mathrm{test}},\ell,D,Q,R,J,r,k,S)

bits of working space.

In plain English

Given degree-at-most-

k

polynomial equations on

n

variables and a design satisfying the layout definition for their factors, the count

N(\mathcal P)

can be computed deterministically in

\poly(n,m_{\mathrm{test}},\ell,D,Q,R,J,r,k,S)\,C_q(2D+1)^{2\tau n}2^{2n/r}

bit operations and polynomial working space, for any

\ell

with

2^\ell>2^n

Why it's here

This specializes the general counting routine to the concrete problem of counting common zeros. It uses the parity-indicator expansion and its truncated-product degree bound to express

N(\mathcal P)

as a quantity of the form the general routine computes, and bounds the cost of evaluating each factor. The layout's row bounds then make the arithmetic polynomial, leaving the exponential cost

C_q(2D+1)^{2\tau n}2^{2n/r}

from the general routine.

Classified routine:

This specializes the paper's general counting routine (prop-general-count) to counting common zeros. It combines the parity-indicator expansion with the row-coefficient bounds, and the remaining work is cost bookkeeping for evaluating each factor.

Uses

propGeneral counting routine and its costlemParity indicator as linear-coefficient h-expansiondefLayout of partitions, measurements, and polynomial rowslemRow coefficients are bounded and constructiblelemTruncated product extracts parity indicators with linear degree

Used by

thmCounting zeros of sparse polynomials fasterclaimPer-branch cost and total exponentclaimPolynomial space by sequential branches

Sources

PaperOpen

Section: §5.4 Cost of evaluating the factors
Page: —
Label: prop:count
Line: main_full_version.tex:3044

Leannot aligned

Phase 2 aligns this node to a Lean declaration.

Friction

info
inferred_dep
the statement's design satisfying Definition is used; the proof relies on the layout's rows and denominators (the \ref in the statement text)
info
inferred_dep
"the rows have common denominator d_den=(R-1)!Q!" is the content of the row-coefficient lemma
info
inferred_dep
critique: Prop 5.3 takes d_H from eq:origin-residue (line 3049). That degree bound and the residue identity come from Lemma total-order: "Lemma bounds the input degree ... By the same lemma, summing their values gives" (lines 3024-3035).