lemmaroutineinferred_dep

Exact negacyclic product with one truncation

Negacyclic product with one truncation in

O(rp\log(rp))

time

pointwise ring product inside the convolution

Lemma·lem:signed-ring-product·§7 Exact normalized polynomial products

Statement (paper)

Let

r=2^\ell<2^p

with integers

\ell\geq1

and

p\geq2

, and fix

C_w>1

. Let

w

be an integer with

p+2\leq w\leq C_wp

. The input supplies

\Gamma(p)\Gamma(r)\Gamma(w)

and two disk grid polynomials

f,g\in\mathcal R_r

in the component format of Proposition with width

w

. One can compute the exact Gaussian integer numerators of

fg

, and then return

Q_p(fg/r)

in that same format, in time

O(rp\log(rp))

on a fixed number of tapes. The output is a disk grid polynomial with error less than

\sqrt2\,2^{-p}

from

fg/r

In plain English

Given two disk grid polynomials

f,g\in\mathcal R_r=\mathbb C[y]/(y^r+1)

with

r=2^\ell<2^p

in the width-

w

component format, one can compute the exact Gaussian integer numerators of

fg

and return

Q_p(fg/r)

in the same format in time

O(rp\log(rp))

. The output is a disk grid polynomial within

\sqrt2\,2^{-p}

fg/r

Why it's here

This is the pointwise polynomial product used for ring multiplication: it packs the coefficients by Kronecker substitution into four big-integer products, reads off exact coefficients, folds them modulo

y^r+1

, and truncates once. Because only the final step rounds, the error is a single

\sqrt2\,2^{-p}

and the output keeps the input format, so later convolution results can call it as a black box at cost

O(rp\log(rp))

per product.

Classified routine:

Standard Kronecker substitution reducing a negacyclic polynomial product with Gaussian integer coefficients to a few big-integer multiplications (as in Schönhage–Strassen and Harvey–van der Hoeven), followed by folding modulo y^r+1 and a single rounding step; the time bound is ordinary bookkeeping.

Uses

propSimultaneous Hadamard layer in near-linear time

Used by

propSynthetic convolution: error, cost, and formatclaimExact normalization identity via retained orderclaimError bound and disk marginclaimTotal cost of transforms and productsclaimComplex convolution via coefficient twistclaimFinal error below 1/2; rounding and carries exact

Inside the proof

claimKronecker evaluation separates product coefficientsclaimSigned carries give two's-complement blocksclaimCentered extraction recovers product coefficientsclaimNegacyclic reduction gives bounded coefficientsclaimTruncation and output format of ring product

Sources

PaperOpen

Section: §7 Exact normalized polynomial products
Page: —
Label: lem:signed-ring-product
Line: sections/06-transforms.tex:463

Leannot aligned

Phase 2 aligns this node to a Lean declaration.

Friction

info
inferred_dep
critique: The statement at sections/06-transforms.tex:468-469 takes its inputs "in the component format of Proposition with width w", but no edge is recorded.