Let \(x\) be an \(n\)-bit Boolean input, that is, a function assigning a Boolean value to each of the \(n\) coordinates. If \(x\) is not the all-zero input — the constant function taking the value \(\mathrm{false}\) everywhere — then there exists a coordinate \(i\) at which \(x\) takes the value \(\mathrm{true}\).

Write \(\mathrm{sgn} : \mathrm{Bool} \to \mathbb {R}\) for the Boolean sign map, which sends \(\mathrm{false}\) to \(1\) and \(\mathrm{true}\) to \(-1\). Then for all Boolean values \(a, b\),

where \(a \oplus b\) denotes the exclusive-or of \(a\) and \(b\); equivalently, \(\mathrm{sgn}\) is a homomorphism from \((\mathrm{Bool}, \oplus )\) to the multiplicative group \(\{ \pm 1\} \).

Let \(\alpha \) be a type, let \(s\) be a finite set of indices from \(\alpha \), and let \(f : \alpha \to \{ \mathrm{false}, \mathrm{true}\} \) be a Boolean-valued function. Write \(\sigma \) for the Boolean sign, so that \(\sigma (\mathrm{false}) = 1\) and \(\sigma (\mathrm{true}) = -1\), and let \(\bigoplus _{i \in s} f(i)\) denote the sum of the values \(f(i)\) taken in the Booleans under exclusive-or, so that this sum equals \(\mathrm{true}\) precisely when an odd number of indices \(i \in s\) satisfy \(f(i) = \mathrm{true}\). Then the sign of this parity equals the product of the individual signs:

For all Boolean values \(a\) and \(b\), the product of their signs satisfies

where \(\mathrm{sign}(\cdot )\) sends \(\mathrm{false}\) to \(1\) and \(\mathrm{true}\) to \(-1\), and \(\mathbf{1}[a \ne b]\) is \(1\) when \(a\) and \(b\) differ and \(0\) when they agree. Equivalently, this product equals \(1\) when the two bits are equal and \(-1\) when they disagree.

Let \(n \in \mathbb {N}\), let \(i \in \mathrm{Fin}\, n\) be a coordinate index, and let \(x\) be an \(n\)-bit Boolean input. The single-coordinate flip of \(x\) at \(i\) — the input obtained from \(x\) by negating its \(i\)-th coordinate and leaving all others unchanged — has value \(\neg \, x_i\) at coordinate \(i\).

Let \(x \colon \mathrm{Fin}\, n \to \mathrm{Bool}\) be an \(n\)-bit Boolean input, and let \(i, j \in \mathrm{Fin}\, n\) be coordinates with \(j \ne i\). Then the input obtained from \(x\) by flipping its \(i\)-th coordinate agrees with \(x\) at coordinate \(j\); that is, its value at \(j\) equals \(x(j)\).

Fix \(n \in \mathbb {N}\), a coordinate \(i \in \mathrm{Fin}\, n\), and an \(n\)-bit Boolean input \(x \colon \mathrm{Fin}\, n \to \mathrm{Bool}\). Writing \(\mathrm{flip}_i\) for the operation that negates the \(i\)-th coordinate of an input and leaves all other coordinates unchanged, applying it twice recovers the original input:

Fix \(n \in \mathbb {N}\) and a coordinate \(i \in \mathrm{Fin}\, n\). On the space of \(n\)-bit Boolean inputs, functions \(\mathrm{Fin}\, n \to \mathrm{Bool}\), consider the single-coordinate flip that negates the \(i\)-th bit of its argument and leaves every other bit unchanged. This map is a bijection.