lemmaroutine
Forward invocation adds; three-stage swap with sign
Forward invocation adds; forward-inverse-forward composition swaps with sign
identifies the net swap effect of the gate networks
Lemma·
lem:scalar-motifs·§3.1 Scalar operations and restored auxiliary valuesStatement (paper)
For arbitrary initial values of its auxiliary wires, a forward
invocation changes to and leaves every other value
unchanged. Performing a forward invocation from to at stage 1,
the inverse forward schedule from to at stage 2, and a forward
invocation from to at stage 3 sends
and restores every auxiliary value. In the bit construction this is the
permutation exchanging and .
In plain English
A forward invocation replaces by and changes nothing else, whatever the initial values of its auxiliary wires. Running a forward invocation from to , then the inverse forward schedule from to , then a forward invocation from to sends to and restores every auxiliary value; in the bit construction this is the permutation swapping and .
Why it's here
This is the basic scalar building block: the three-stage composition is a signed swap of two registers that leaves scratch wires clean. The bit and complex motif interface results use it to identify the net effect of the network as the permutation exchanging and and fixing the scratch roles.
Classified routine:
A direct calculation in the style of the classical three-XOR/three-shear swap, a well-known reversible-computing identity in which three shears compose to a signed swap. Applied here to the paper's forward-invocation primitive, with bookkeeping showing that the auxiliary wires are restored.
Uses
Nothing else in the paper
Used by
Sources
PaperOpen
- Section
- §3.1 Scalar operations and restored auxiliary values
- Page
- —
- Label
lem:scalar-motifs- Line
sections/03-motifs.tex:89
Leannot aligned
Phase 2 aligns this node to a Lean declaration.