claimroutineinferred_dep

Truncation and output format of ring product

Truncation after shifting gives

Q_p(fg/r)

in the input format

finishes the ring product's output format

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

Statement (paper)

For each

j

, the

p

-bit grid numerator of the normalized product is

\operatorname{trunc}_0\left(\Re H_j/2^{p+\ell}\right)+i\operatorname{trunc}_0\left(\Im H_j/2^{p+\ell}\right)

, and it is computed by shifting the absolute magnitude right by

p+\ell

bits and restoring the sign, at cost

O(p)

per coefficient. The returned coefficient

2^{-p}

times this numerator equals

Q_p(2^{-2p}H_j/r)

, so it satisfies the error and disk bounds of . Each component numerator has magnitude at most

2^p

and is written as a signed

w

-bit two's-complement word in the stated order, at cost

O(rw)=O(rp)

, which gives the format used by the opposite transform; the total cost is dominated by four exact integer products.

In plain English

Truncating

\Re H_j

and

\Im H_j

after dividing by

2^{p+\ell}

gives the

p

-bit grid numerator of

Q_p(fg/r)

, computed by a sign-restoring right shift in

O(p)

time per coefficient. The resulting numerators have magnitude at most

2^p

and are written as signed

w

-bit two's-complement words, so the whole step costs

O(rp)

beyond the four exact integer products.

Why it's here

This finishes the lemma's proof. Since

H_j

is the exact folded coefficient and

|H_j|\leq r2^{2p}

, the shifted value is

2^p

times

fg/r

rounded toward zero, so it satisfies the same error and disk bounds as

Q_p

. Writing it as

w

-bit words restores the input format, and the total cost is dominated by the four exact integer products, giving

O(rp\log(rp))

overall.

Classified routine:

Bookkeeping step: truncation toward zero by a sign-restoring right shift and writing the results in two's-complement format. It follows directly from the bound |H_j| ≤ r2^{2p} in the previous claim and the definition of Q_p, via standard fixed-point arithmetic cost accounting.

Uses

claimNegacyclic reduction gives bounded coefficients

Used by

Nothing in the paper

Sources

PaperOpen

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

Leannot aligned

Phase 2 aligns this node to a Lean declaration.

Friction

info
inferred_dep
outline: "Truncation, output format and total cost" rests on claim-lem-signed-ring-product-4