claimroutineinferred_dep

Summing group costs gives total time

Summing group costs gives total O(V(Lτ+1))O(V(L^\tau+1)) under the asymptotics
totals the per-group costs into the lemma's bound
Claim·§A Packed additions on grouped rectangles·inside lemPacked selected-bit XOR on grouped streams

Statement (paper)

Put δbad=min⁡{1,80(f−1)2−K}\delta_{\rm bad}=\min\{1,80(f-1)2^{-K}\}. Then the total time of the procedure, including the descriptor work, is O ⁣(V(Lτ+1)+MA3+δbadMA(R+A))O\!\left(V(L^\tau+1)+MA^3+\delta_{\rm bad}MA(R+A)\right), which is . Moreover, when A=O(p)A=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 two additional terms divided by V=MRV=MR are bounded by A3/RA^3/R and 80(f−1)2−KA(1+A/R)80(f-1)2^{-K}A(1+A/R), both o(1)o(1), and these bounds depend on the supplied groups only through M,R,AM,R,A.

In plain English

With δbad=min⁡{1,80(f−1)2−K}\delta_{\rm bad}=\min\{1,80(f-1)2^{-K}\}, the whole procedure, descriptor work included, runs in time O(V(Lτ+1)+MA3+δbadMA(R+A))O(V(L^\tau+1)+MA^3+\delta_{\rm bad}MA(R+A)). Under the stated asymptotic conditions, the two extra terms divided by V=MRV=MR are at most A3/RA^3/R and 80(f−1)2−KA(1+A/R)80(f-1)2^{-K}A(1+A/R), both o(1)o(1) and depending on the groups only through M,R,AM,R,A.

Why it's here

This finishes the parent lemma by adding up the per-group rectangular costs from the rectangle lemma. Each group is a rectangle with Aν=O(A)A_\nu=O(A) and the processing overhead is O(Vν)O(V_\nu) plus a final O(V)O(V) rewind. The group record counts and volumes sum to MM and VV, so the local bounds collapse to the stated total, and the asymptotic condition makes the extra terms negligible.
Classified routine:
Direct summation of the per-group costs from the rectangle lemma (lem-packed-selected-bit-rectangle) over groups whose record counts and volumes total M and V, followed by elementary asymptotic bounds on the two extra terms.

Uses

lemPacked XOR of selected address bitsclaimEach group collapses to a single rectangleclaimGroup-by-group processing on fixed tapes

Used by

Nothing in the paper

Sources

PaperOpen
Section
§A Packed additions on grouped rectangles
Page
—
Label
—
Line
sections/11-grouped-rectangles.tex:133
Leannot aligned

Phase 2 aligns this node to a Lean declaration.

Friction

  • info
    inferred_dep
    outline: "Summing local rectangle bounds gives the time" rests on claim-lem-packed-selected-bit-addition-2
  • info
    inferred_dep
    outline: "Summing local rectangle bounds gives the time" rests on claim-lem-packed-selected-bit-addition-3