claimroutineinferred_dep

Each group collapses to a single rectangle

Each group collapses to a single rectangle with O(A3)O(A^3) descriptor cost
reduces grouped streams to the rectangle lemma
Claim·§A Packed additions on grouped rectangles·inside lemPacked selected-bit XOR on grouped streams

Statement (paper)

For each group ν\nu, after collapsing the row ordinal and the spectator fields into the four positive lengths N0,N1,N2,N3N_0,N_1,N_2,N_3, the group together with the current order of the names x,y,zx,y,z is exactly the rectangle of Lemma , with MνM_\nu records and volume VνV_\nu. Fixing a collapsed coordinate fixes every one of its mixed-radix factors, so the rectangular algorithm preserves the row ordinal and all original spectator coordinates, and forming the local descriptor from the template and length vector takes O(A3)O(A^3) time per group.

In plain English

For each group ν\nu, merging the row ordinal and spectator fields into four lengths N0,N1,N2,N3N_0,N_1,N_2,N_3 makes the group, with the current order of x,y,zx,y,z, exactly a rectangle as in the rectangular lemma, with MνM_\nu records and volume VνV_\nu. The collapse preserves the row ordinal and all spectator coordinates, and building the local descriptor takes O(A3)O(A^3) time per group.

Why it's here

This lets the single-rectangle packed XOR procedure be applied to each group directly, so the grouped lemma reduces to a sum of rectangular costs. Fixing a collapsed coordinate fixes all its mixed-radix factors, so the rectangular algorithm leaves the row ordinal and spectators untouched. The O(A3)O(A^3) descriptor cost uses the uniform bound Aν=O(A)A_\nu=O(A) from the previous claim, and later claims use it to total the time over groups.
Classified routine:
Direct bookkeeping: the group is reduced to the rectangular case of lem-packed-selected-bit-rectangle by collapsing mixed-radix coordinates into four lengths, and the descriptor cost follows from the A_ν=O(A) bound in the preceding claim.

Uses

lemPacked XOR of selected address bitsclaimDescriptor bounds give A_ν=O(A)

Used by

claimGroup-by-group processing on fixed tapesclaimSumming group costs gives total time

Sources

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

Phase 2 aligns this node to a Lean declaration.

Friction

  • info
    inferred_dep
    outline: "Each group collapses to a single rectangle" rests on claim-lem-packed-selected-bit-addition-1