Manuscript Oai279-A@1 · Oai279-A.tex · lemma · a1abc73f

Lemma: Action of one row block

Stage 6: the explicit circuit for the frozen input › The complete gate-list expansion rule · lines 902–930 · proof included or linked

Oai279-A@1#lem:row

Back to manuscript

On scratch-zero inputs, row $m$ acts as

∣ x, y, 000 ⟩ ⟼ ∣ x, y \oplus ([x = m] e_{m}), 000 ⟩,

where $e_{m}$ is the output word whose one positions are $T_{m}$ . The statement holds for arbitrary output word $y$ .

Proof. After the initial NOT gates, input bit $j$ equals one exactly when its original value matches bit $j$ of $m$ . The three scratch computations therefore give

u = x^{'}_{0} x^{'}_{1}, v = x^{'}_{0} x^{'}_{1} x^{'}_{2}, f = x^{'}_{0} x^{'}_{1} x^{'}_{2} x^{'}_{3} = [x = m] .

The CNOTs XOR $e_{m}$ into $y$ exactly when this predicate is one. The reversed conjunction chain restores $f, v, u$ to zero, since no input bit changed during the target operations. The final NOTs restore the original input.

All these are identities on basis vectors, with no relative phase. Linearity extends the identity to their superpositions.

Displayed formulas in this passage

unlabeled · line 905
$∣ x, y, 000 ⟩ ⟼ ∣ x, y \oplus ([x = m] e_{m}), 000 ⟩,$
unlabeled · line 918
$u = x^{'}_{0} x^{'}_{1}, v = x^{'}_{0} x^{'}_{1} x^{'}_{2}, f = x^{'}_{0} x^{'}_{1} x^{'}_{2} x^{'}_{3} = [x = m] .$

Nearby in this section

section: The complete gate-list expansion rule