Controlled-Z update in the binary phase representation (source code)

= Controlled-Z update in the binary phase representation
{title2=$b_j'=b_j\oplus a_k,\quad b_k'=b_k\oplus a_j,\quad s'=s+2a_ja_k$}

Conjugation by a <Controlled-Z gate> leaves the $a$ bits unchanged and updates the displayed $b$ bits and phase, using the old bits. The phase occurs when the extra $Z$ from one line is moved past $X$ on the other line. These constant-size updates support <Heisenberg propagation of a Pauli observable through a Clifford circuit>.