claimroutineinferred_dep

Centered extraction recovers product coefficients

Centered carry scan recovers exact product coefficients in O(rp)O(rp)
reads off coefficients of the big product
Claim·§7 Exact normalized polynomial products·inside lemExact negacyclic product with one truncation

Statement (paper)

Let ZZ be one of the four signed product integers, let hh be its corresponding ordinary polynomial product padded by hJ−1=0h_{J-1}=0 with J=2rJ=2r, and write Z=∑j=0J−1qjB0j+εB0JZ=\sum_{j=0}^{J-1}q_jB_0^j+\varepsilon B_0^J with 0≤qj<B00\leq q_j<B_0 and ε∈{−1,0}\varepsilon\in\{-1,0\}. Then the centered extraction recurrence ρ0=0\rho_0=0, h^j∈[−B0/2,B0/2)\widehat h_j\in[-B_0/2,B_0/2) with h^j≡qj+ρj(modB0)\widehat h_j\equiv q_j+\rho_j\pmod{B_0}, ρj+1=(qj+ρj−h^j)/B0\rho_{j+1}=(q_j+\rho_j-\widehat h_j)/B_0 has carries ρj∈{0,1}\rho_j\in\{0,1\} and satisfies h^j=hj\widehat h_j=h_j for all 0≤j<J0\leq j<J, with final carry ρJ=−ε\rho_J=-\varepsilon; hence all coefficients of hh are extracted by a single scan of JJ blocks in time O(rp)O(rp).

In plain English

For each signed product integer Z=∑j<JqjB0j+εB0JZ=\sum_{j<J} q_jB_0^j+\varepsilon B_0^J with J=2rJ=2r, a centered-remainder carry scan produces digits h^j∈[−B0/2,B0/2)\widehat h_j\in[-B_0/2,B_0/2) with h^j=hj\widehat h_j=h_j for every j<Jj<J. The carries stay in {0,1}\{0,1\}, the final carry is −ε-\varepsilon, and one scan of JJ blocks takes O(rp)O(rp) time.

Why it's here

Since every coefficient of hh has ∣hj∣<B0/2|h_j|<B_0/2 (first claim), hjh_j is the unique centered residue of ZZ's digit plus carry. This lets the scan read the signed product coefficients straight from the two's-complement blocks of the big-integer product (second claim). The later negacyclic reduction step then uses these exact coefficients.
Classified routine:
Standard Kronecker-substitution unpacking with balanced (centered) digit recovery. Since the coefficients are bounded by B0/2B_0/2 (earlier claim), signed digits follow from the two's-complement blocks by a routine carry scan.

Uses

claimKronecker evaluation separates product coefficientsclaimSigned carries give two's-complement blocks

Used by

claimNegacyclic reduction gives bounded coefficients

Sources

PaperOpen
Section
§7 Exact normalized polynomial products
Page
—
Label
—
Line
sections/06-transforms.tex:528
Leannot aligned

Phase 2 aligns this node to a Lean declaration.

Friction

  • info
    inferred_dep
    outline: "Centered extraction recovers product coefficients" rests on claim-lem-signed-ring-product-1
  • info
    inferred_dep
    outline: "Centered extraction recovers product coefficients" rests on claim-lem-signed-ring-product-2