claimroutine

Eight controlled additions flip parity

Eight controlled additions flip a parity when the control is 1
arithmetic core of the packed XOR step
Claim·§5.2 Packed changes of selected address bits·inside lemPacked XOR of selected address bits

Statement (paper)

For a Boolean control cc and arbitrary integers u,wu,w, the eight operations , performed in the displayed order with every predicate evaluated on the current values, do nothing if c=0c=0, and if c=1c=1 they produce (u′,w′)=(u+c(1−2(u mod 2)), w)(u',w')=\bigl(u+c(1-2(u\bmod2)),\,w\bigr), where u mod 2∈{0,1}u\bmod2\in\{0,1\} also for negative uu. Thus the parity of uu is flipped precisely when c=1c=1, both quotients under division by two are preserved, the auxiliary integer ww is restored, and each coordinate is displaced from its initial value by at most four at every stage.

In plain English

For a Boolean control cc and integers u,wu,w, the eight prescribed controlled additions, applied in order with predicates evaluated on current values, do nothing when c=0c=0. When c=1c=1 they change uu to u+(1−2(u mod 2))u+(1-2(u\bmod 2)) (flipping its parity, with u mod 2∈{0,1}u\bmod 2\in\{0,1\} even for negative uu) and leave ww unchanged.

Why it's here

This is the arithmetic core of the XOR step: it shows the eight additions act as a conditional parity flip, preserving both quotients by two and restoring the auxiliary integer ww, with every coordinate moving by at most four at any stage. The next claim uses this to compare the packed cyclic-shift implementation with the ideal XOR away from a bad set.
Classified routine:
A direct case check over the parity of u and the control bit c, a small bookkeeping verification of a specific gadget (eight controlled additions) built for the paper's packed XOR step; it relies on no deep known result.

Uses

Nothing else in the paper

Used by

claimPacked shifts match ideal XOR off bad set

Sources

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

Phase 2 aligns this node to a Lean declaration.