claimroutineinferred_dep

Total cost and asymptotic simplification

Total cost O(V(Lτ+1))O(V(L^\tau+1)) once repair terms become o(V)o(V)
sums the step costs into the lemma's bound
Claim·§5.2 Packed changes of selected address bits·inside lemPacked XOR of selected address bits

Statement (paper)

The procedure runs on a fixed number of tapes in time O ⁣(V(Lτ+1)+MArect3+δbadMArect(R+Arect))O\!\left(V(L^\tau+1)+MA_{\rm rect}^3+\delta_{\rm bad}MA_{\rm rect}(R+A_{\rm rect})\right), which is . Moreover, when Arect=O(p)A_{\rm rect}=O(p), RR exceeds every fixed polynomial in pp, f≤d≤pf\le d\le p and K/log⁡p→∞K/\log p\to\infty, the terms MArect3MA_{\rm rect}^3 and δbadMArect(R+Arect)\delta_{\rm bad}MA_{\rm rect}(R+A_{\rm rect}) are o(V)o(V), since after division by V=MRV=MR they are at most Arect3/R→0A_{\rm rect}^3/R\to0 and 80(f−1)2−KArect(1+Arect/R)=O(p22−K(1+Arect/R))=o(1)80(f-1)2^{-K}A_{\rm rect}(1+A_{\rm rect}/R)=O(p^22^{-K}(1+A_{\rm rect}/R))=o(1), so the total time is O(V(Lτ+1))O(V(L^\tau+1)).

In plain English

The procedure runs on a fixed number of tapes in time O(V(Lτ+1)+MArect3+δbadMArect(R+Arect))O(V(L^\tau+1)+MA_{\rm rect}^3+\delta_{\rm bad}MA_{\rm rect}(R+A_{\rm rect})). Under the stated asymptotic conditions (Arect=O(p)A_{\rm rect}=O(p), RR beyond every fixed polynomial in pp, f≤d≤pf\le d\le p, K/log⁡p→∞K/\log p\to\infty), the last two terms are o(V)o(V), so the total is O(V(Lτ+1))O(V(L^\tau+1)).

Why it's here

This claim adds up the costs of the earlier steps: the rotations and swaps give the VLτVL^\tau term, the sorting-based repair of the exceptional set gives the MArect3MA_{\rm rect}^3 and δbad\delta_{\rm bad} terms, and the top-position XOR adds only O(V)O(V). Dividing by V=MRV=MR shows the repair terms are at most Arect3/RA_{\rm rect}^3/R and O(p22−K(1+Arect/R))O(p^2 2^{-K}(1+A_{\rm rect}/R)), both tending to zero, so they are negligible next to the main term.
Classified routine:
Direct bookkeeping: sums the costs from the earlier claims (rotations, sorting-based repair, top-position XOR) and checks by elementary asymptotics that the repair terms are o(V) under the stated parameter conditions.

Uses

claimBad set is small and invariantclaimRotations cost O(V L^τ) via swapsclaimRepair exceptional records by sortingclaimTop selected position by two-bit XOR

Used by

Nothing in the paper

Sources

PaperOpen
Section
§5.2 Packed changes of selected address bits
Page
—
Label
—
Line
sections/05-layers.tex:433
Leannot aligned

Phase 2 aligns this node to a Lean declaration.

Friction

  • info
    inferred_dep
    outline: "Total cost and asymptotic simplification" rests on claim-lem-packed-selected-bit-rectangle-3
  • info
    inferred_dep
    outline: "Total cost and asymptotic simplification" rests on claim-lem-packed-selected-bit-rectangle-4
  • info
    inferred_dep
    outline: "Total cost and asymptotic simplification" rests on claim-lem-packed-selected-bit-rectangle-5
  • info
    inferred_dep
    outline: "Total cost and asymptotic simplification" rests on claim-lem-packed-selected-bit-rectangle-6