claimroutine

Top selected position by two-bit XOR

Top selected bit handled by a plain two-bit XOR in

O(V)

completes the XOR on the last position

Claim·§5.2 Packed changes of selected address bits·inside lemPacked XOR of selected address bits

Statement (paper)

After

T_0

has been implemented, applying the two-bit XOR

y_{j_{f-1}}\leftarrow y_{j_{f-1}}\oplus x_{j_{f-1}}

by Lemma , with the chunks

x,y

split at the selected positions and the other intervals collapsed, uses a descriptor with a fixed number of positive lengths, each at most

V

, and costs

O(V)

. This supplies the omitted selected position

j_{f-1}

, and when

f=1

the maps

S_0,T_0

are identities,

\mathcal B

is empty, and this step is the entire algorithm.

In plain English

Once the procedure

T_0

for the other selected positions is in place, the remaining position

j_{f-1}

is handled by a single two-bit XOR

y_{j_{f-1}}\leftarrow y_{j_{f-1}}\oplus x_{j_{f-1}}

O(V)

time. When

f=1

the maps

S_0,T_0

are identities,

\mathcal B

is empty, and this step is the whole algorithm.

Why it's here

This step completes the XOR on all

f

selected positions by adding the one position that

T_0

omitted. It uses the elementary stream operations of Lemma lem:elementary-streams, with

x,y

split at the selected positions and other intervals collapsed, so the descriptor has a fixed number of lengths, each at most

V

, and the cost is only linear. The

f=1

case shows the construction is consistent in the degenerate setting.

Classified routine:

Direct application of the paper's elementary-stream lemma (lem-elementary-streams) to perform a single two-bit XOR in linear time; pure bookkeeping inside the packed selected-bit XOR construction.

Uses

lemElementary digit scans run in linear time

Used by

claimTotal cost and asymptotic simplification

Sources

PaperOpen

Section: §5.2 Packed changes of selected address bits
Page: —
Label: —
Line: sections/05-layers.tex:425

Leannot aligned

Phase 2 aligns this node to a Lean declaration.