lemmaroutineinferred_dep

Packed selected-bit XOR on grouped streams

XORs selected bits across grouped streams in O(V(Lτ+1))O(V(L^\tau+1)) time
side result extending the rectangle lemma to groups
Lemma·lem:packed-selected-bit-addition·§A Packed additions on grouped rectangles

Statement (paper)

Let a valid grouped packed stream of Definition  be supplied, and let A≥2A\ge2 bound the actual total bit length of its descriptor D\mathcal D, including the header and the entry for RR. At the 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) in every group. It fixes the group, row ordinal, spectator coordinates, all other chunk bits, and every record payload; in particular, the chunk zz is restored. For V=MRV=MR, its time is O ⁣(V(Lτ+1)+MA3+Mmin⁡{1,80(f−1)2−K} A(R+A)). O\!\left(V(L^\tau+1)+MA^3+ M\min\{1,80(f-1)2^{-K}\}\,A(R+A)\right). 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, this is O(V(Lτ+1))O(V(L^\tau+1)), uniformly over the group counts, shapes, and payloads whose supplied descriptors satisfy that bound.

In plain English

Given a valid grouped packed stream whose descriptor has total bit length at most AA, one fixed multitape procedure XORs xjix_{j_i} into yjiy_{j_i} at positions ji=ρ+iKj_i=\rho+iK (0≤i<f0\le i<f) in every group, restoring the chunk zz and leaving everything else unchanged. With V=MRV=MR it runs in time O(V(Lτ+1)+MA3+Mmin⁡{1,80(f−1)2−K}A(R+A))O(V(L^\tau+1)+MA^3+M\min\{1,80(f-1)2^{-K}\}A(R+A)), which is O(V(Lτ+1))O(V(L^\tau+1)) under the stated asymptotic conditions.

Why it's here

This extends the single-rectangle packed XOR lemma to grouped streams, where groups have different shapes. Each group is collapsed to one rectangle, processed locally with the rectangular algorithm, and written back; the per-group costs are then summed using the uniform O(A)O(A) bound on descriptor integers. The extra terms are negligible relative to VV under the asymptotic hypotheses, independent of group counts and shapes.
Classified routine:
Direct extension of the paper's single-rectangle packed XOR lemma (lem:packed-selected-bit-rectangle) to grouped streams. Each group is collapsed to one rectangle, processed with the rectangular routine, and written back, with per-group costs summed via the O(A) descriptor bound; this is standard multitape bookkeeping.

Uses

lemPacked XOR of selected address bitsdefGrouped packed stream format

Used by

Nothing in the paper

Inside the proof

claimDescriptor bounds give A_ν=O(A)claimEach group collapses to a single rectangleclaimGroup-by-group processing on fixed tapesclaimSumming group costs gives total time

Sources

PaperOpen
Section
§A Packed additions on grouped rectangles
Page
—
Label
lem:packed-selected-bit-addition
Line
sections/11-grouped-rectangles.tex:61
Leannot aligned

Phase 2 aligns this node to a Lean declaration.

Friction

  • info
    inferred_dep
    critique: The lemma statement (sections/11-grouped-rectangles.tex:63-64) opens with "Let a valid grouped packed stream of Definition  be supplied", but the DAG has no edge to the definition, which therefore shows up as an orphan.