claimroutineinferred_dep

Disk margins and error propagation through transforms

All stages keep disk-grid inputs in the disk, with explicit error bounds
chains stage errors without clipping
Claim·§9.7 Precision and exact recovery·inside thmInteger multiplication in O(n (lg n)^{1-κ}) time

Statement (paper)

For all sufficiently large nn (enforced by one fixed cutoff such as b≥224b\ge2^{24} together with the other eventual construction conditions), every call of the synthetic ring convolution, the complex convolution M~C\widetilde{\mathcal M}_{\mathbb C}, the chirp map C~\widetilde{\mathscr C}, and the source transform and its opposite maps disk-grid inputs of the stated norms (one operand of norm at most .7.7, chirp input of norm at most .6.6, source input of norm at most .5.5) to disk-grid arrays without clipping, and their errors are as follows: Ering=M(3L+2)<5TLE_{\rm ring}=M(3L+2)<5TL for the normalized ring convolution, ∥M~C(f,g)−MC(f,g)∥<6TLhp\|\widetilde{\mathcal M}_{\mathbb C}(f,g)-\mathcal M_{\mathbb C}(f,g)\|<6TLh_p, ∥C~(x)−QFtx∥<8TLhp\|\widetilde{\mathscr C}(x)-QF_{\boldsymbol t}x\|<8TLh_p with ∥C~(x)∥<.701\|\widetilde{\mathscr C}(x)\|<.701, and the scaled source transform has error less than EshpE_sh_p with Es=9 2γTLE_s=9\,2^\gamma TL and norm at most .5+Eshp<.501.5+E_sh_p<.501.

In plain English

For sufficiently large nn, the synthetic ring convolution, the complex convolution M~C\widetilde{\mathcal M}_{\mathbb C}, the chirp map C~\widetilde{\mathscr C} and the source transform with its opposite always take disk-grid inputs of the stated norms (.7, .6, .5) to disk-grid outputs without clipping. Their errors are bounded by Ering=M(3L+2)<5TLE_{\rm ring}=M(3L+2)<5TL, 6TLhp6TLh_p, 8TLhp8TLh_p (with ∥C~(x)∥<.701\|\widetilde{\mathscr C}(x)\|<.701), and EshpE_sh_p with Es=9 2γTLE_s=9\,2^\gamma TL (norm at most .5+Eshp<.501.5+E_sh_p<.501) respectively.

Why it's here

This claim fixes the numerical bookkeeping: each computed stage is shown to stay inside the unit disk, so the black-box convolution, chirp and source-transform procedures can be chained, and their error bounds accumulate in a controlled way. It builds on the synthetic convolution and transform error bounds, the complex twist, the chirp and source procedures, and the tensor resampling error. The resulting explicit constants feed the final argument that the total error stays below 1/2, so rounding and carries are exact.
Classified routine:
Numerical error bookkeeping that chains the paper's earlier error bounds (synthetic convolution, the chirp and source procedures, tensor resampling) in the style of the precision analysis of Harvey–van der Hoeven (2021). It checks that each stage stays inside the disk and adds up the explicit constants.

Uses

claimComplex convolution via coefficient twistclaimChirp transform and source transform procedurespropSynthetic convolution: error, cost, and formatlemCost and accuracy of synthetic transformpropSimultaneous Hadamard layer in near-linear timelemTensor resampling across d dimensions

Used by

claimFinal error below 1/2; rounding and carries exact

Sources

PaperOpen
Section
§9.7 Precision and exact recovery
Page
—
Label
—
Line
sections/08-assembly.tex:558
Leannot aligned

Phase 2 aligns this node to a Lean declaration.

Friction

  • info
    inferred_dep
    outline: "Disk margins and error propagation through transforms" rests on claim-thm-main-5
  • info
    inferred_dep
    outline: "Disk margins and error propagation through transforms" rests on claim-thm-main-6
  • info
    inferred_dep
    outline: "Disk margins and error propagation through transforms" rests on prop:synthetic-convolution
  • info
    inferred_dep
    outline: "Disk margins and error propagation through transforms" rests on lem:synthetic-transform-cost
  • info
    inferred_dep
    outline: "Disk margins and error propagation through transforms" rests on prop:simultaneous-layer
  • info
    inferred_dep
    outline: "Disk margins and error propagation through transforms" rests on lem:tensor-resampling