claimroutine

Uniform bound on packed-child width parameter

Packed children have width parameter

A_*\le C_Ap

uniform width bound for packed-call costs

Claim·§5.4 An explicit guard-width bound·inside propSimultaneous Hadamard layer in near-linear time

Statement (paper)

Put

\Delta=\lceil C_0d^{C_1}\rceil

and

R_{\rm g}=2r(p+2\Delta+3)

. For all sufficiently large

p

\Delta\le p

2rp\le R_{\rm g}\le12rp

, and every packed child with

M_{\rm child}

records has rectangular width parameter

A_*=\lceil\log_2(2M_{\rm child}R_{\rm g})\rceil\le\lceil\log_2(4MR_{\rm g})\rceil\le C_Ap

, where

C_A=C_M+b_r+7

In plain English

With

\Delta=\lceil C_0d^{C_1}\rceil

and

R_{\rm g}=2r(p+2\Delta+3)

, for all large

p

we have

\Delta\le p

and

2rp\le R_{\rm g}\le12rp

. Every packed child with

M_{\rm child}

records then has rectangular width parameter

A_*=\lceil\log_2(2M_{\rm child}R_{\rm g})\rceil\le\lceil\log_2(4MR_{\rm g})\rceil\le C_Ap

, where

C_A=C_M+b_r+7

Why it's here

This claim turns the size assumptions on

d

r

and

M

into a single linear bound

C_Ap

on the width parameter of every packed child. Because

d\approx p^\epsilon

and

\epsilon C_1<1

, the guard width

\Delta

is far below

p

, so

R_{\rm g}

is within a constant factor of

rp

. The later cost estimates for packed basis changes use this uniform bound.

Classified routine:

Direct arithmetic bookkeeping: since

d\approx p^\epsilon

with

\epsilon C_1<1

, the guard width satisfies

\Delta=o(p)

, and taking logarithms of the size assumptions on

M

and

r

gives a bound linear in

p

. No new idea is involved.

Uses

Nothing else in the paper

Used by

claimPacked basis changes cost uniformly near-linear

Sources

PaperOpen

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

Leannot aligned

Phase 2 aligns this node to a Lean declaration.