claimroutineinferred_dep
Exact power-of-two scaling and output format
Scaling by is exact and adds only low zero bits
fixes the output format and width
Claim·§7.1 The normalized convolution interface·inside propSynthetic convolution: error, cost, and format
Statement (paper)
The final scaling by the power of two preserves the -bit grid and is performed exactly: appending zero bits at the least significant end of each signed -bit numerator returned by the opposite procedure gives its exact two's-complement encoding in bits, including for negative values, with the real word preceding the imaginary word and the coefficient order unchanged. Since and , the output width is , and writing takes time.
In plain English
Multiplying by at the end is exact: appending zero low-order bits to each signed -bit numerator gives its two's-complement encoding in bits, negative values included, with real-before-imaginary order and coefficient order unchanged. The width is , and writing takes time.
Why it's here
This finishes the proposition's output claims. The scaling by in the exact identity from the first claim adds no rounding error and stays on the -bit grid, so the only remaining task is the output format. The width bound , keeps the descriptor and format cost within the stated budget.
Classified routine:
Direct bookkeeping fact: multiplying a two's-complement integer by 2^m is a left shift appending m zero bits, so the encoding stays exact. The O(p) width and descriptor-writing cost follow from the stated bounds w ≤ C_w p and m_M ≤ C_ℓ p.
Uses
Used by
Nothing in the paper
Sources
PaperOpen
- Section
- §7.1 The normalized convolution interface
- Page
- —
- Label
—- Line
sections/06-transforms.tex:720
Leannot aligned
Phase 2 aligns this node to a Lean declaration.
Friction
- infoinferred_depoutline: "Exact power-of-two scaling and output format" rests on claim-prop-synthetic-convolution-1