lemmaroutineinferred_dep

Cost and accuracy of synthetic transform

Synthetic transforms cost

O(Tp[dK+pK^{\tau-1}+\ell d^{\lambda'}])

transform stage of the synthetic convolution

Lemma·lem:synthetic-transform-cost·§6.2 A layout on which the parallel layers apply

Statement (paper)

Fix the rational parameters and positive comparison constants

a_d\leq b_d

a_r\leq b_r

of Proposition . Fix constants

C_\ell>0

and

C_w>1

, and choose the layer constants once as

C_M=C_\ell+1,\qquad C_{\rm desc}=32(C_\ell+C_w+1).

Use these constants and

C_w

in Proposition . These fixed choices determine a cutoff

p_1

, one fixed-tape procedure, and an implicit time constant with the following guarantee. For every choice of positive integers

p,d,r

with

p\geq p_1

and

a_dp^\epsilon\leq d\leq b_dp^\epsilon,\qquad 2^{a_rp/d}\leq r\leq2^{b_rp/d},

suppose

d\geq2

and

r=2^\ell

with an integer

2\leq\ell<p

, and require

d\ell\leq C_\ell p,\qquad 1\leq K=\lfloor d^c\rfloor\leq\ell-1.

Let

t_i\in\{2^{\ell-1},2^\ell\}

for

1\leq i\leq d-1

, put

M=\prod_{i=1}^{d-1}t_i

and

T=rM

, and let

w

be an integer with

p+2\leq w\leq C_wp

. The cutoff and time constant are independent of

p,d,r

, these axis choices, the round headers constructed from them, and

w

within the displayed bounds. The input supplies the self-delimiting header

\mathcal T=\Gamma(p)\Gamma(d)\Gamma(r)\Gamma(K)\Gamma(w) \prod_{i=1}^{d-1}\Gamma(t_i),

where the product is concatenation in axis order and

\Gamma

is the integer code of . The supplied

d

determines the number of axis entries, and

\ell=\log_2r

is obtained from the supplied power of two

r

. Assume that the header is valid with the stated values and that the input records use the two's-complement component format of Proposition with width

w

. The procedure constructs an explicit positional layout permutation

L

of record addresses, preserving their polynomial suffixes, and transforms disk grid arrays of

M

contiguous degree-less-than-

r

polynomial records. Its exact counterpart is

LB F_{\boldsymbol t}^-

. Its opposite procedure consumes that order and has exact counterpart

F_{\boldsymbol t}^+B^{-1}L^{-1}

. Each procedure has error less than

\sqrt2\ell\,2^{-p}

, returns disk grid coefficients in the same component format, and costs

O\left(Tp\left[dK+pK^{\tau-1}+\ell d^{\lambda'}\right]\right).

Both layout construction and final restoration are charged in this bound. The forward procedure may retain its output layout for a pointwise product and the following opposite procedure.

In plain English

Under the stated size bands and constraints on

p,d,r,K,w

, a fixed-tape procedure builds a layout permutation

L

and computes the forward transform

LBF_{\boldsymbol t}^-

on disk grid arrays of

M

polynomial records, and an opposite procedure computes

F_{\boldsymbol t}^+B^{-1}L^{-1}

. Each has error less than

\sqrt2\ell 2^{-p}

, keeps the same component format, and costs

O(Tp[dK+pK^{\tau-1}+\ell d^{\lambda'}])

including layout construction and restoration.

Why it's here

This is the cost and accuracy guarantee for the transform stage of the synthetic ring multiplication. The proof builds a chunk-grouped layout with the chunk-swap lemma, handles the prefix slots bit by bit, and runs the simultaneous Hadamard layer once per round with a single truncation each. This gives the three cost terms and the error bound of

\ell

truncations. The retained layout lets the convolution proposition do a pointwise product between a forward and an opposite transform without restoring the original order in between.

Classified routine:

Assembles the synthetic transform from the paper's simultaneous Hadamard layer proposition and its chunk-swap lemma. The cost and error bounds come from summing ℓ rounds, each with one truncation, plus the layout permutations, which is bookkeeping over the earlier nodes.

Uses

propSimultaneous Hadamard layer in near-linear timelemSwapping binary address chunks in O(Vu^τ)

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 twistclaimDisk margins and error propagation through transformsclaimCost table yields the final time bound

Inside the proof

claimLayout permutation by moves and chunk exchangesclaimHeader parsing and list setup costclaimEach layout round meets layer hypothesesclaimPrefix-slot rounds evaluated bit by bitclaimTwiddle rotations without coefficient sortingclaimOne truncation per round bounds errorclaimFull procedures include layout conjugation

Sources

PaperOpen

Section: §6.2 A layout on which the parallel layers apply
Page: —
Label: lem:synthetic-transform-cost
Line: sections/06-transforms.tex:171

Leannot aligned

Phase 2 aligns this node to a Lean declaration.

Friction

info
inferred_dep
The proof says exchanges of nonadjacent width-K address chunks each cost O(TpK^τ). That cost is the fixed-τ chunk-exchange bound, but the lemma is not named or numbered, so this link is inferred.