claimroutineinferred_dep

Packed basis changes cost uniformly near-linear

Packed basis changes cost

O(M_{\rm child}R_{\rm g}(L^\tau+1))

uniformly

gives one common constant for the cost recurrence

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

Statement (paper)

Uniformly over all allowed

d,r

and all large

p

, one has

f\le d\le p

K\ge\tfrac12a_d^c p^{\epsilon c}

and

r\ge2^{(a_r/b_d)p^{1-\epsilon}}

, and the two additional normalized terms in , namely

A_*^3/R_{\rm g}

and

80(f-1)2^{-K}A_*(1+A_*/R_{\rm g})

, tend to zero. Hence Lemma has the required

O(M_{\rm child}R_{\rm g}(L^\tau+1))

cost for every packed call, with one common time constant.

In plain English

Uniformly over all allowed

d,r

and all large

p

, we have

f\le d\le p

K\ge\tfrac12a_d^c p^{\epsilon c}

and

r\ge2^{(a_r/b_d)p^{1-\epsilon}}

, and the extra terms

A_*^3/R_{\rm g}

and

80(f-1)2^{-K}A_*(1+A_*/R_{\rm g})

in the packed-rectangle time bound tend to zero. Hence the packed selected-bit rectangle lemma gives cost

O(M_{\rm child}R_{\rm g}(L^\tau+1))

for every packed call, with one common time constant.

Why it's here

The packed selected-bit rectangle lemma has cost terms that are only negligible under asymptotic conditions. Here those conditions are checked uniformly in the parameter range.

K

and

r

are bounded below by the size assumptions on

d

and

r

A_*\le C_Ap

from the previous claim, together with

R_{\rm g}\ge 2rp

and

r

growing like

2^{p^{1-\epsilon}}

, makes

A_*^3/R_{\rm g}

vanish. The

2^{-K}

factor kills the other term. The resulting bound with a single constant is what the later recurrence analysis uses to sum packed basis-change costs.

Classified routine:

This is an asymptotic parameter check. It plugs the bound

A_*\le C_Ap

from the previous claim,

R_{\rm g}\ge 2rp

, and the size assumptions on

d,r

into the cost bound of the packed selected-bit rectangle lemma, and verifies that the extra terms vanish.

Uses

lemPacked XOR of selected address bitsclaimUniform bound on packed-child width parameter

Used by

claimRecurrence total cost and conversion to H

Sources

PaperOpen

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

Leannot aligned

Phase 2 aligns this node to a Lean declaration.

Friction

info
inferred_dep
outline: "Packed basis changes cost uniformly linear-ish" rests on claim-prop-simultaneous-layer-1