lemmaroutine

Lifted indicator coefficients have small height

Lemma·lem:rational-lift-height·§B.1 Integer coefficients of the lifted indicator

Statement (paper)

Write

e_j(Y)=a_j+b_jY

for

0\le j<\ell

. Then

a_j,b_j\in\mathbb Z

and

|a_j|,|b_j|\le2^{C\ell^2}\qquad(0\le j<\ell)

for an absolute constant

C

. Successive division of

p_\ell

h

constructs these polynomials using

\poly(\ell)

bit operations and bits of working space.

In plain English

Writing

e_j(Y)=a_j+b_jY

for

0\le j<\ell

, the coefficients

a_j

and

b_j

are integers with absolute value at most

2^{C\ell^2}

for an absolute constant

C

. They can be computed by successively dividing

p_\ell

h

using

\poly(\ell)

bit operations and bits of working space.

Why it's here

This gives the integrality and the explicit size bound on the coefficients of the degree-at-most-one polynomials

e_j

, which the construction in the rational idempotent lemma needs. The polynomial-time, polynomial-space computation by repeated division makes that construction effective, not merely existent.

Classified routine:

A height bound on coefficients produced by repeated polynomial division by a monic integer polynomial (base-h expansion of p_ell), following from standard estimates on Euclidean division over Z; it is bookkeeping supporting the paper's idempotent construction, not a new idea.

Uses

Nothing else in the paper

Used by

lemParity indicator as linear-coefficient h-expansion

Sources

PaperOpen

Section: §B.1 Integer coefficients of the lifted indicator
Page: —
Label: lem:rational-lift-height
Line: main_full_version.tex:3916

Leannot aligned

Phase 2 aligns this node to a Lean declaration.