lemmaroutine

Packed XOR of selected address bits

XORs ff selected bits of chunk xx into yy in O(V(Lτ+1))O(V(L^\tau+1)) time
local step summed by the Hadamard layer and grouped lemma
Lemma·lem:packed-selected-bit-rectangle·§5.2 Packed changes of selected address bits

Statement (paper)

Let R≥1R\ge1, K≥6K\ge6, f≥1f\ge1, L=fKL=fK, and 0≤ρ<K0\le\rho<K. Let N0,N1,N2,N3N_0,N_1,N_2,N_3 be positive integers, and let (χ1,χ2,χ3)(\chi_1,\chi_2,\chi_3) be a permutation of (x,y,z)(x,y,z). Consider RR-bit records in lexicographic order on [N0]×[2L]χ1×[N1]×[2L]χ2×[N2]×[2L]χ3×[N3]. [N_0]\times[2^L]_{\chi_1}\times[N_1]\times[2^L]_{\chi_2} \times[N_2]\times[2^L]_{\chi_3}\times[N_3]. The subscript names the chunk at that position. The input supplies N0,…,N3,R,K,f,ρN_0,\ldots,N_3,R,K,f,\rho as a fixed number of canonical binary integers, together with the finite permutation of the chunk names, as in Section . Put M=23L∏h=03Nh,V=MR,Arect=⌈log⁡2(2V)⌉. M=2^{3L}\prod_{h=0}^3N_h,\qquad V=MR,\qquad A_{\rm rect}=\lceil\log_2(2V)\rceil. At the selected positions ji=ρ+iKj_i=\rho+iK, numbered from the least significant bit, one fixed multitape procedure performs yji⟵yji⊕xji(0≤i<f). y_{j_i}\longleftarrow y_{j_i}\mathbin\oplus x_{j_i} \quad(0\le i<f). It preserves the spectator coordinates, all other chunk bits, and every record payload; in particular, it restores the entire chunk zz for every initial value. With δbad=min⁡{1,80(f−1)2−K}\delta_{\rm bad}=\min\{1,80(f-1)2^{-K}\}, its time is 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). 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, this is O(V(Lτ+1))O(V(L^\tau+1)), uniformly over the permitted lengths and payloads in the fixed family.

In plain English

On a stream of RR-bit records indexed by a rectangle with three chunks of L=fKL=fK bits each (named x,y,zx,y,z in some order), one multitape procedure XORs xjix_{j_i} into yjiy_{j_i} at the ff positions ji=ρ+iKj_i=\rho+iK, leaving all else unchanged and restoring chunk zz. It runs 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})), which is O(V(Lτ+1))O(V(L^\tau+1)) under the stated asymptotic conditions.

Why it's here

This lemma gives the basic cost bound for a packed change of ff selected address bits on one rectangle, which is the local step that later lemmas on grouped packed streams sum over. The idea is to implement f−1f-1 of the XORs by a constant number of packed cyclic shifts, which are cheap by the chunk-swap and affine-stream lemmas and correct away from a small bad set. The few exceptional records are then repaired by sorting, and the last position is handled by a plain two-bit XOR, so the total is dominated by the VLτV L^\tau term.
Classified routine:
A technical cost lemma that combines the paper's earlier chunk-swap, affine-stream and elementary-stream lemmas through packed cyclic shifts, then repairs the small bad set by sorting. It is bookkeeping and an adaptation of earlier nodes, not a headline idea.

Inside the proof

Sources

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

Phase 2 aligns this node to a Lean declaration.