claimroutineinferred_dep

Negacyclic reduction gives bounded coefficients

Negacyclic folding gives coefficients

|H_j|\le r2^{2p}

within

O(p)

bits

bounds folded coefficients for truncation

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

Statement (paper)

Reducing the real and imaginary numerator streams

ac-be

and

ae+bc

modulo

y^r+1

gives Gaussian integer coefficients

H_j

, each a sum of exactly

r

signed products of Gaussian integer input coefficients of modulus at most

2^p

, so

|H_j|\leq r2^{2p}

. Moreover

\|fg/r\|_\infty\leq\|f\|_\infty\|g\|_\infty

, so the normalized product of disk polynomials lies in the disk, and all intermediate coefficient additions fit in

O(p)

bits without overflow or ambiguity between adjacent packing fields.

In plain English

Reducing the real and imaginary numerator streams modulo

y^r+1

yields Gaussian integer coefficients

H_j

, each a signed sum of exactly

r

products of input coefficients, so

|H_j|\leq r2^{2p}

. The normalized product

fg/r

stays in the disk since

\|fg/r\|_\infty\leq\|f\|_\infty\|g\|_\infty

, and all intermediate additions fit in

O(p)

bits without overflow or ambiguity between packing fields.

Why it's here

The exact product coefficients recovered by centered extraction are folded modulo

y^r+1

to get the ring product, and this claim bounds the folded values

H_j

r2^{2p}

. That bound shows the later truncation step stays in the disk and that the arithmetic stays within

O(p)

bits, so the

Q_p

rounding and output format can be handled in the next claim.

Classified routine:

A direct coefficient bound for negacyclic convolution: each coefficient of a product modulo y^r+1 is a signed sum of r products, so the triangle inequality gives |H_j| ≤ r2^{2p}. This is standard bookkeeping that follows from the preceding extraction claim.

Uses

claimCentered extraction recovers product coefficients

Used by

claimTruncation and output format of ring product

Sources

PaperOpen

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

Leannot aligned

Phase 2 aligns this node to a Lean declaration.

Friction

info
inferred_dep
outline: "Negacyclic reduction and normalized product in disk" rests on claim-lem-signed-ring-product-3