claimroutineinferred_dep
Transform sizes and precision satisfy band bounds
Sizes , , ,
fixes the parameter scales for later lemmas
Statement (paper)
For all sufficiently large , the parameters , , , , , and satisfy , , , and , with the explicit bounds and , so that one may take , , , . Moreover, with and , one has , and eventually, and for .
In plain English
For large , with , , , , and the smallest such power of two with , one has , , and , with explicit bounds and . Also, with and , we get , , and once .
Why it's here
This pins down how the dimension, transform length, radix and guard-width parameters scale with the word size , so later steps can invoke the layer and cost-table results with explicit constants (, , , ). The bound (and for large ) shows the guard region is negligible next to the precision, and it relies on the exponent choices checked in the previous claim, such as .
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.
Uses
Used by
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
- infoinferred_depoutline: "Transform sizes and precision satisfy band bounds" rests on claim-thm-main-1