claimroutineinferred_dep

Guarded evaluation with single final truncation

Guard width is o(p)o(p), so one final truncation gives error <2 2−p<\sqrt2\,2^{-p}
gives the error bound and output format
Claim·§5.4 An explicit guard-width bound·inside propSimultaneous Hadamard layer in near-linear time

Statement (paper)

The guard width ⌈C0dC1⌉\lceil C_0d^{C_1}\rceil is o(p)o(p) uniformly over the allowed dd, so every intermediate coefficient of the exact evaluation of Hz\mathcal H z is represented exactly in the stated O(p)O(p) width. Every row of H\mathcal H has absolute row sum one, so Hz\mathcal H z lies in the complex unit disk and so does Qp(Hz)Q_p(\mathcal H z). The single final truncation satisfies ∥Qp(Hz)−Hz∥∞<2 2−p\|Q_p(\mathcal H z)-\mathcal H z\|_\infty<\sqrt2\,2^{-p}, and the truncated numerators have magnitude at most 2p2^p, so they fit in the supplied component width ww.

In plain English

The guard width ⌈C0dC1⌉\lceil C_0d^{C_1}\rceil is o(p)o(p) uniformly over allowed dd, so all intermediate coefficients of the exact evaluation of Hz\mathcal H z fit exactly in O(p)O(p) width. Since H\mathcal H has absolute row sums one, Hz\mathcal H z and Qp(Hz)Q_p(\mathcal H z) lie in the unit disk, the single final truncation has error below 2 2−p\sqrt2\,2^{-p} in sup norm, and the truncated numerators are at most 2p2^p so they fit in width ww.

Why it's here

Having converted the computed exact CC-layer into H\mathcal H, this step controls precision: because ϵC1<1\epsilon C_1<1 and d≤bdpϵd\le b_dp^\epsilon, the guard width is negligible next to pp, so nothing is rounded until the one final truncation. This gives the proposition its error bound and shows the output format fits in the supplied component width.
Classified routine:
Direct precision bookkeeping: since εC_1<1 and d ≤ b_d p^ε, the guard width is o(p). The unit row-sum bound and the single componentwise rounding estimate (error √2·2^{-p}) follow from elementary norm inequalities and the earlier exact-evaluation claim.

Uses

claimRecurrence total cost and conversion to H

Used by

Nothing in the paper

Sources

PaperOpen
Section
§5.4 An explicit guard-width bound
Page
—
Label
—
Line
sections/05-layers.tex:979
Leannot aligned

Phase 2 aligns this node to a Lean declaration.

Friction

  • info
    inferred_dep
    outline: "Exact guarded evaluation and single truncation error" rests on claim-prop-simultaneous-layer-3