claimroutine

Kronecker evaluation separates product coefficients

Kronecker evaluation at

2^{4p}

keeps product coefficients below

B_0/2

setup for packing coefficients into big integers

Claim·§7 Exact normalized polynomial products·inside lemExact negacyclic product with one truncation

Statement (paper)

Write

f=2^{-p}(a+ib)

and

g=2^{-p}(c+ie)

with

a,b,c,e\in\mathbb Z[y]

of degree less than

r

and coefficients of absolute value at most

2^p

, and set

B_0=2^{4p}

and

A_u=u(B_0)=\sum_{j=0}^{r-1}u_jB_0^j

for

u\in\{a,b,c,e\}

. Then

|A_u|\leq2^p\frac{B_0^r-1}{B_0-1}<B_0^r/2

, so each magnitude fits in

4pr

bits. Moreover, each evaluation product

A_aA_c,A_bA_e,A_aA_e,A_bA_c

equals

\sum_{j=0}^{2r-2}h_jB_0^j

, where

h

is the corresponding ordinary product in

\mathbb Z[y]

, and every coefficient satisfies

|h_j|\leq r2^{2p}<2^{3p}<B_0/2

In plain English

Evaluating the integer polynomials

a,b,c,e

B_0=2^{4p}

gives integers

A_u

of magnitude below

B_0^r/2

(so at most

4pr

bits). Each product such as

A_aA_c

equals the evaluation at

B_0

of the ordinary polynomial product

h

, and every coefficient of

h

satisfies

|h_j|\leq r2^{2p}<2^{3p}<B_0/2

Why it's here

This is the Kronecker-substitution setup for the parent lemma: because the product coefficients are far smaller than

B_0/2

, they do not overlap when packed into one large integer. That lets a single big-integer multiplication carry all the coefficients of

fg

, which the later claims unpack with signed carries and centered extraction.

Classified routine:

Standard Kronecker substitution (Kronecker; Schönhage 1982) with elementary coefficient bounds. The node only checks the size estimates (e.g. |h_j| <= r 2^{2p} < B_0/2) that ensure the packed coefficients do not overlap.

Uses

Nothing else in the paper

Used by

claimSigned carries give two's-complement blocksclaimCentered extraction recovers product coefficients

Sources

PaperOpen

Section: §7 Exact normalized polynomial products
Page: —
Label: —
Line: sections/06-transforms.tex:476

Leannot aligned

Phase 2 aligns this node to a Lean declaration.