claimroutineinferred_dep

Group-by-group processing on fixed tapes

Groups processed one at a time on fixed tapes with O(Vν)O(V_\nu) overhead
multitape implementation of the per-group reduction
Claim·§A Packed additions on grouped rectangles·inside lemPacked selected-bit XOR on grouped streams

Statement (paper)

Using separate outer input and output tapes with forward cursors, each group ν\nu can be copied into a local area, processed there by the complete rectangular algorithm, its output appended to the outer output tape, and the visited local area cleared, reusing the same local and primitive work tapes for every group. The copy, append, positioning and cleanup cost O(Vν)O(V_\nu) per group and one final outer rewind costs O(V)O(V); the inner routine restores its local work tapes within its stated bound, so the tape count is fixed and no local call scans an earlier or later group.

In plain English

Each group can be copied from the outer input tape to a local area, processed there by the rectangular algorithm, and appended to the outer output tape, with the local area cleared afterwards, all on a fixed set of tapes. The copy, append, positioning and cleanup cost O(Vν)O(V_\nu) per group plus an O(V)O(V) final rewind, and no local call scans any other group.

Why it's here

This turns the per-group rectangle reduction into an actual multitape implementation. Because each group's overhead is only O(Vν)O(V_\nu) and the inner routine restores its work tapes, the total time is the sum of the rectangular costs plus O(V)O(V), which the next claim totals into the stated bound.
Classified routine:
Standard multitape Turing machine bookkeeping: copying each group to a local work area, running the rectangular routine there, appending the output and clearing the area costs linear time per group. It is a direct implementation step on top of the preceding per-group rectangle reduction.

Uses

claimEach group collapses to a single rectangle

Used by

claimSumming group costs gives total time

Sources

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

Phase 2 aligns this node to a Lean declaration.

Friction

  • info
    inferred_dep
    outline: "Group-by-group processing on fixed local tapes" rests on claim-lem-packed-selected-bit-addition-2