claimroutineinferred_dep

Repair exceptional records by sorting

Sorting exceptional records by destination repairs T0T_0
repairs the bad set at MA3MA^3 cost
Claim·§5.2 Packed changes of selected address bits·inside lemPacked XOR of selected address bits

Statement (paper)

After the movement S0S_0, the correction implements T0T_0 on the entire stream: scanning with a record-rank counter, one extracts the records whose addresses lie in B\mathcal B, computes for each current exceptional address qq its destination q′=T0(S0−1(q))q'=T_0(S_0^{-1}(q)) with destination rank rank⁡(q′)=rank⁡(q)+∑h∈{x,y,z}(qh′−qh)σh\operatorname{rank}(q')=\operatorname{rank}(q)+\sum_{h\in\{x,y,z\}}(q'_h-q_h)\sigma_h, and stably radix sorts the extracted records by these distinct keys, which are exactly the ranks of the marked holes, then reinserts them in one forward scan. Each per-record computation (rank counter, membership test in B\mathcal B, and the address q′q') takes O(Arect3)O(A_{\rm rect}^3) time.

In plain English

After the movement S0S_0, the ideal map T0T_0 is realized on the whole stream by extracting the records at exceptional addresses in B\mathcal B, computing each one's destination q′=T0(S0−1(q))q'=T_0(S_0^{-1}(q)) and its rank, stably radix sorting them by these distinct destination ranks, and reinserting them in one forward scan. Each per-record computation (rank counter, test for membership in B\mathcal B, address q′q') costs O(Arect3)O(A_{\rm rect}^3).

Why it's here

Since T0S0−1T_0S_0^{-1} fixes everything outside B\mathcal B and only permutes B\mathcal B, only the exceptional records need to move. The destination ranks are exactly the ranks of the marked holes, so sorting by them puts each record in its correct slot. This gives the deterministic repair step whose cost is the MArect3MA_{\rm rect}^3 term and the δbad\delta_{\rm bad} term in the total time bound.
Classified routine:
A standard Turing-machine bookkeeping step: extract the few exceptional records, compute their destination ranks, stably radix sort them, and merge them back in one forward scan. It follows directly from the earlier claim that T0S0−1T_0S_0^{-1} only permutes the small bad set B\mathcal B.

Uses

claimBad set is small and invariant

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:395
Leannot aligned

Phase 2 aligns this node to a Lean declaration.

Friction

  • info
    inferred_dep
    outline: "Deterministic repair by sorting exceptional records" rests on claim-lem-packed-selected-bit-rectangle-3