claimroutineinferred_dep

Bad set is small and invariant

Bad set has size ≤δbadM\le\delta_{\rm bad}M and is invariant under both maps
restricts the repair to few exceptional records
Claim·§5.2 Packed changes of selected address bits·inside lemPacked XOR of selected address bits

Statement (paper)

The bad set satisfies ∣B∣≤δbadM|\mathcal B|\le\delta_{\rm bad}M. The ideal map T0T_0 preserves all guard values and hence preserves B\mathcal B; since T0T_0 and S0S_0 are bijections that agree off B\mathcal B, we have S0(Bc)=T0(Bc)=BcS_0(\mathcal B^c)=T_0(\mathcal B^c)=\mathcal B^c and S0(B)=BS_0(\mathcal B)=\mathcal B, so T0S0−1T_0S_0^{-1} fixes Bc\mathcal B^c and permutes B\mathcal B.

In plain English

The bad set B\mathcal B of addresses has size at most δbadM\delta_{\rm bad}M. The ideal map T0T_0 preserves B\mathcal B and its complement, and S0S_0 does too, so T0S0−1T_0S_0^{-1} fixes every address outside B\mathcal B and only permutes B\mathcal B.

Why it's here

This turns the agreement of S0S_0 and T0T_0 off B\mathcal B into a usable repair structure. The correction T0S0−1T_0S_0^{-1} acts only on the at most δbadM\delta_{\rm bad}M exceptional addresses, which gives the δbad\delta_{\rm bad} term in the time bound. The invariance of B\mathcal B under both maps lets the exceptional records be identified, sorted and fixed in place.
Classified routine:
The claim is elementary bookkeeping that follows from the previous claim that S0S_0 agrees with T0T_0 off B\mathcal B. Two bijections that agree off a set they both preserve differ only by a permutation of that set, and the size bound ∣B∣≤δbadM|\mathcal B|\le\delta_{\rm bad}M is a direct count.

Uses

claimPacked shifts match ideal XOR off bad set

Used by

claimRepair exceptional records by sortingclaimTotal cost and asymptotic simplification

Sources

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

Phase 2 aligns this node to a Lean declaration.

Friction

  • info
    inferred_dep
    outline: "Bad set small and preserved by both maps" rests on claim-lem-packed-selected-bit-rectangle-2