lemmaroutine

Parity indicator as linear-coefficient h-expansion

Lemma·lem:rational-idempotent·§5.1 An integer polynomial for one equation

Statement (paper)

For every integer

\ell\ge1

, one can construct polynomials

e_0,\ldots,e_{\ell-1}\in\mathbb Z[Y]

, each of degree at most one, such that

p_\ell(Y)=\sum_{j=0}^{\ell-1}e_j(Y)h(Y)^j, \qquad p_\ell(y)\equiv\mathds{1}_{\{2\mid y\}}\pmod{2^\ell} \quad(y\in\mathbb Z).

The coefficients of the

e_j

have

\poly(\ell)

bits, and the construction uses

\poly(\ell)

bit operations and

\poly(\ell)

bits of space.

In plain English

For every

\ell\ge1

one can construct integer polynomials

e_0,\ldots,e_{\ell-1}

, each of degree at most one, such that

p_\ell(Y)=\sum_{j<\ell}e_j(Y)h(Y)^j

, where

p_\ell(y)\equiv\mathbb 1_{\{2\mid y\}}\pmod{2^\ell}

for all integers

y

. The

e_j

have

\poly(\ell)

-bit coefficients and are computed with

\poly(\ell)

bit operations and space.

Why it's here

This rewrites the mod-

2^\ell

parity indicator

p_\ell

as a sum of powers of

h

with only degree-at-most-one coefficients, which is the form later lemmas use when they substitute integers

y_i

and treat the powers of

h(y_i)

as a polynomial in an auxiliary variable

V

. The integrality, the bit-size bound, and the efficient construction all come from the repeated division by

h

controlled by the height bound of Lemma B.1.

Classified routine:

This is Hensel-style lifting of the parity idempotent modulo 2^ℓ, written as a base-h(Y) expansion with linear digits (h presumably Y(Y-1) or similar) via repeated division by h. It follows directly from the height bound of Lemma B.1 and standard polynomial division.

Uses

lemLifted indicator coefficients have small height

Used by

lemTruncated product extracts parity indicators with linear degreepropCost of counting solutions via factor evaluationlemCounting zeros of sparse polynomial systemsclaimMultilinear incidence polynomial with linear degreeclaimTest-group entries by subset inversion

Sources

PaperOpen

Section: §5.1 An integer polynomial for one equation
Page: —
Label: lem:rational-idempotent
Line: main_full_version.tex:2887

Leannot aligned

Phase 2 aligns this node to a Lean declaration.