claimroutineinferred_dep

Transform sizes and precision satisfy band bounds

Sizes Tp=Θ(n)Tp=\Theta(n), d=Θ(pϵ)d=\Theta(p^\epsilon), ℓ=Θ(p1−ϵ)\ell=\Theta(p^{1-\epsilon}), γ=o(b)\gamma=o(b)
fixes the parameter scales for later lemmas
Claim·§9.2 Input and transform sizes·inside thmInteger multiplication in O(n (lg n)^{1-κ}) time

Statement (paper)

For all sufficiently large nn, the parameters b=⌈log⁡2n⌉b=\lceil\log_2n\rceil, p=6bp=6b, d=⌊bϵ⌋d=\lfloor b^\epsilon\rfloor, K=⌊dc⌋K=\lfloor d^c\rfloor, T∈[4n/b,8n/b)T\in[4n/b,8n/b), r=2⌈(log⁡2T)/d⌉r=2^{\lceil(\log_2T)/d\rceil} and ℓ=log⁡2r\ell=\log_2r satisfy Tp=Θ(n)Tp=\Theta(n), d=Θ(pϵ)d=\Theta(p^\epsilon), K=Θ(pϵc)K=\Theta(p^{\epsilon c}), ℓ=Θ(p1−ϵ)\ell=\Theta(p^{1-\epsilon}) and r=2Θ(p1−ϵ)r=2^{\Theta(p^{1-\epsilon})}, with the explicit bounds 112pϵ≤d≤pϵ\frac1{12}p^\epsilon\le d\le p^\epsilon and p12d≤ℓ≤p3d\frac{p}{12d}\le\ell\le\frac{p}{3d}, so that one may take ad=ar=1/12a_d=a_r=1/12, bd=1b_d=1, br=1/3b_r=1/3, Cℓ=1C_\ell=1. Moreover, with α=⌈(12d2b)1/4⌉\alpha=\lceil(12d^2b)^{1/4}\rceil and γ=2dα2\gamma=2d\alpha^2, one has γ<28b2/3\gamma<28b^{2/3}, 2≤α<p2\le\alpha<\sqrt p and γ=o(b)\gamma=o(b) eventually, and γ≤b/4\gamma\le b/4 for b≥224b\ge2^{24}.

In plain English

For large nn, with b=⌈log⁡2n⌉b=\lceil\log_2 n\rceil, p=6bp=6b, d=⌊bϵ⌋d=\lfloor b^\epsilon\rfloor, K=⌊dc⌋K=\lfloor d^c\rfloor, T∈[4n/b,8n/b)T\in[4n/b,8n/b) and r=2ℓr=2^\ell the smallest such power of two with r≥T1/dr\ge T^{1/d}, one has Tp=Θ(n)Tp=\Theta(n), d=Θ(pϵ)d=\Theta(p^\epsilon), K=Θ(pϵc)K=\Theta(p^{\epsilon c}) and ℓ=Θ(p1−ϵ)\ell=\Theta(p^{1-\epsilon}), with explicit bounds 112pϵ≤d≤pϵ\frac1{12}p^\epsilon\le d\le p^\epsilon and p12d≤ℓ≤p3d\frac{p}{12d}\le\ell\le\frac{p}{3d}. Also, with α=⌈(12d2b)1/4⌉\alpha=\lceil(12d^2b)^{1/4}\rceil and γ=2dα2\gamma=2d\alpha^2, we get γ<28b2/3\gamma<28b^{2/3}, 2≤α<p2\le\alpha<\sqrt p, γ=o(b)\gamma=o(b) and γ≤b/4\gamma\le b/4 once b≥224b\ge2^{24}.

Why it's here

This pins down how the dimension, transform length, radix and guard-width parameters scale with the word size pp, so later steps can invoke the layer and cost-table results with explicit constants (ad=ar=1/12a_d=a_r=1/12, bd=1b_d=1, br=1/3b_r=1/3, Cℓ=1C_\ell=1). The bound γ=o(b)\gamma=o(b) (and γ≤b/4\gamma\le b/4 for large bb) shows the guard region is negligible next to the precision, and it relies on the exponent choices checked in the previous claim, such as ϵ<1/12\epsilon<1/12.
Classified routine:
Elementary parameter bookkeeping: the asymptotic and explicit bounds follow by direct calculation from the definitions of b, p, d, T, r and α, using the exponent constraints (e.g. ε<1/12) verified in the previous claim.

Sources

PaperOpen
Section
§9.2 Input and transform sizes
Page
—
Label
—
Line
sections/08-assembly.tex:50
Leannot aligned

Phase 2 aligns this node to a Lean declaration.

Friction

  • info
    inferred_dep
    outline: "Transform sizes and precision satisfy band bounds" rests on claim-thm-main-1