claimroutineinferred_dep

Signed carries give two's-complement blocks

Signed carries lie in {−1,0}\{-1,0\}, giving two's-complement blocks
handles signs in the big-integer products
Claim·§7 Exact normalized polynomial products·inside lemExact negacyclic product with one truncation

Statement (paper)

Let u=(u0,…,ur−1)u=(u_0,\dots,u_{r-1}) be the integer coefficient vector of the evaluated polynomial, with Au=∑j=0r−1ujB0jA_u=\sum_{j=0}^{r-1}u_jB_0^j. Define γ0=0\gamma_0=0, dj≡uj+γj(modB0)d_j\equiv u_j+\gamma_j\pmod{B_0} with 0≤dj<B00\leq d_j<B_0, and γj+1=(uj+γj−dj)/B0\gamma_{j+1}=(u_j+\gamma_j-d_j)/B_0. Then every carry γj\gamma_j lies in {−1,0}\{-1,0\} and Au=∑j=0r−1djB0j+γrB0rA_u=\sum_{j=0}^{r-1}d_jB_0^j+\gamma_rB_0^r, so the rr blocks djd_j of 4p4p bits form a fixed-width two's-complement encoding of AuA_u with γr=−1\gamma_r=-1 exactly when Au<0A_u<0, and the blocks of ∣Au∣|A_u| can be obtained from them in O(rp)O(rp) time by a constant number of scans.

In plain English

For an integer coefficient vector uu with Au=∑ujB0jA_u=\sum u_jB_0^j, the carries γj\gamma_j from reducing each uj+γju_j+\gamma_j into [0,B0)[0,B_0) all lie in {−1,0}\{-1,0\}, giving Au=∑djB0j+γrB0rA_u=\sum d_jB_0^j+\gamma_rB_0^r. So the rr blocks djd_j of 4p4p bits form a fixed-width two's-complement encoding of AuA_u, with γr=−1\gamma_r=-1 exactly when Au<0A_u<0, and the blocks of ∣Au∣|A_u| follow in O(rp)O(rp) time by a constant number of scans.

Why it's here

This lets signed Kronecker integers be handled as ordinary nonnegative bit strings, so the big-integer multiplication can work with the signs of the coefficients. The key point is that the coefficients are small relative to B0B_0 (from the previous claim), which keeps every carry in {−1,0}\{-1,0\}. The later centered-extraction claim then reads the product coefficients back from these blocks.
Classified routine:
Standard carry propagation and two's-complement encoding argument for Kronecker substitution with signed coefficients. It follows directly from the coefficient bound in the previous claim (|u_j| small relative to B_0), which keeps the carries in {-1,0}.

Uses

claimKronecker evaluation separates product coefficients

Used by

claimCentered extraction recovers product coefficients

Sources

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

Phase 2 aligns this node to a Lean declaration.

Friction

  • info
    inferred_dep
    outline: "Signed packing via bounded-carry blocks" rests on claim-lem-signed-ring-product-1