propositionroutineinferred_dep

Synthetic convolution: error, cost, and format

Approximates normalized convolution with error

<\sqrt2 M(3\ell+1)2^{-p}

convolution black box for the complex convolution

Proposition·prop:synthetic-convolution·§7.1 The normalized convolution interface

Statement (paper)

Under the hypotheses of Lemma ,

\mathcal M_r

on disk grid operands has an approximation with error less than

\sqrt2\,M(3\ell+1)2^{-p}

and cost

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

Put

m_M=\log_2M

and

w_M=w+m_M

. The returned grid array is in the original array and coefficient order, with the same two's-complement component format at width

w_M

. The procedure supplies

\Gamma(w_M)

on the output descriptor tape, so the caller knows every component boundary from this width and the retained shape parameters. If one operand has norm at most

\rho<1

and the bound in is at most

1-\rho

, the returned grid array is a disk array.

In plain English

The normalized convolution

\mathcal M_r

on disk grid operands can be approximated with error less than

\sqrt2\,M(3\ell+1)2^{-p}

in time

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

. The output keeps the original array and coefficient order, with two's-complement components of width

w_M=w+\log_2 M

and

\Gamma(w_M)

on the descriptor tape, and it is a disk array when one operand has norm at most

\rho<1

and the error bound is at most

1-\rho

Why it's here

This packages the synthetic transforms and the signed ring product into a single convolution black box with explicit error, cost and output format. It runs two forward transforms,

M=T/r

pointwise ring products and one opposite transform, then scales exactly by

M

. The result gives the later complex-convolution and error-propagation arguments a ready-made interface with a disk-margin guarantee.

Classified routine:

Direct packaging of the synthetic transform lemma and the signed ring product lemma: the usual transform–pointwise multiply–inverse transform convolution, with error bookkeeping and a triangle-inequality disk-margin check. It adds no new idea beyond those earlier nodes.

Uses

lemExact negacyclic product with one truncationlemCost and accuracy of synthetic transform

Used by

claimComplex convolution via coefficient twistclaimDisk margins and error propagation through transforms

Inside the proof

claimExact normalization identity via retained orderclaimError bound and disk marginclaimExact power-of-two scaling and output formatclaimTotal cost of transforms and products

Sources

PaperOpen

Section: §7.1 The normalized convolution interface
Page: —
Label: prop:synthetic-convolution
Line: sections/06-transforms.tex:633

Leannot aligned

Phase 2 aligns this node to a Lean declaration.

Friction

info
inferred_dep
critique: The statement at sections/06-transforms.tex:635 begins "Under the hypotheses of Lemma ". The proof also runs its forward and opposite procedures, so the statement-level edge is missing.