lemmaroutine

Truncated product extracts parity indicators with linear degree

Lemma·lem:total-order·§5.2 Keeping the product degree linear

Statement (paper)

Let

m_{\mathrm{test}}\ge0

and

\ell\ge1

be integers. For integers

y_1,\ldots,y_{m_{\mathrm{test}}}

, put

B_i(V)=\sum_{j=0}^{\ell-1}e_j(y_i)h(y_i)^jV^j.

Then

\mathcal S_\ell\!\Bigl(\prod_{i=1}^{m_{\mathrm{test}}} B_i(V)\bmod V^\ell\Bigr) \equiv\prod_{i=1}^{m_{\mathrm{test}}}\mathds{1}_{\{2\mid y_i\}}\pmod{2^\ell}.

For any nonnegative integer

d_*

, if the

y_i

are instead polynomials over

\mathbb Q

of total degree at most

d_*

, then each retained coefficient of

V^s

, and hence their sum, has total input degree at most

d_*(m_{\mathrm{test}}+2(\ell-1))

In plain English

For integers

y_i

, the product of the

B_i(V)

truncated mod

V^\ell

, after applying

\mathcal S_\ell

(the operation that sums the retained coefficients of

V^s

), is congruent mod

2^\ell

to the product of the indicators that each

y_i

is even. If the

y_i

are instead rational polynomials of total degree at most

d_*

, each retained coefficient, and hence their sum, has total degree at most

d_*(m_{\mathrm{test}}+2(\ell-1))

Why it's here

This combines the per-factor expansion of the parity indicator from Lemma 5.1 into a product over many tests. The product is truncated mod

V^\ell

, so each

V^s

coefficient has

h

-weight at most

\ell-1

, which keeps the total degree linear in

m_{\mathrm{test}}+\ell

rather than multiplying by

\ell

for every factor. That linear degree bound is what the counting results that use this lemma rely on.

Classified routine:

Follows directly from the per-factor expansion in Lemma 5.1: multiplying the factors, truncating mod V^ℓ (since h(y) is divisible by 2 when y is even, so higher powers vanish mod 2^ℓ) and counting degrees is straightforward bookkeeping.

Uses

lemParity indicator as linear-coefficient h-expansion

Used by

propCost of counting solutions via factor evaluationlemCounting zeros of sparse polynomial systemsclaimMultilinear incidence polynomial with linear degree

Sources

PaperOpen

Section: §5.2 Keeping the product degree linear
Page: —
Label: lem:total-order
Line: main_full_version.tex:2958

Leannot aligned

Phase 2 aligns this node to a Lean declaration.