claimroutineinferred_dep

Three shears interchange the two chunks

Three shears swap the chunks, only the middle one needing the circuit
reduces chunk swap to one circuit shear
Claim·§4.2 Transferring a finite circuit to address permutations·inside propPower-width chunk interchange in O(Ve^τ)

Statement (paper)

Let HH and DD denote the contents of the two address chunks, viewed as componentwise values. Then the three updates D←D−HD\leftarrow D-H, H←H+DH\leftarrow H+D, D←H−DD\leftarrow H-D, performed in this order, send (H,D)(H,D) to (D,H)(D,H), so they interchange the two chunks. Only the middle update H←H+DH\leftarrow H+D uses the circuit, while the other two target the later group and have linear cost.

In plain English

Applying D←D−HD\leftarrow D-H, then H←H+DH\leftarrow H+D, then D←H−DD\leftarrow H-D sends (H,D)(H,D) to (D,H)(D,H), so the two chunks are swapped. Only the middle update H←H+DH\leftarrow H+D needs the circuit; the other two target the later group and cost linear time.

Why it's here

This is the classical swap by three shears: the values go (H,D)→(H,D−H)→(D,D−H)→(D,H)(H,D)\to(H,D-H)\to(D,D-H)\to(D,H). It reduces the chunk interchange to one circuit-based shear, supplied by the previous claim, plus two cheap linear-cost updates from the affine-update lemma, which gives the recurrence in the next claim.
Classified routine:
This is the classical swap-by-three-shears identity, (H,D)→(H,D−H)→(D,D−H)→(D,H), a direct calculation. The cost accounting follows from the previous claim (circuit shear) and the affine-update lemma.

Uses

claimCircuit on role streams realizes shearlemAffine updates on digit fields cost linear time

Used by

claimRecurrence solves to O(e^τ) per volume

Sources

PaperOpen
Section
§4.2 Transferring a finite circuit to address permutations
Page
—
Label
—
Line
sections/04-swap.tex:189
Leannot aligned

Phase 2 aligns this node to a Lean declaration.

Friction

  • info
    inferred_dep
    outline: "Three shears interchange the two chunks" rests on claim-prop-power-interchange-2
  • info
    inferred_dep
    outline: "Three shears interchange the two chunks" rests on lem:ordered-affine-streams