## The well known formulas

Most readers will be familiar with `-x = ~x + 1 = ~(x - 1)`. These are often just stated without justification, or even an explanation for why they are equivalent. There are some algebraic tricks, but I don't think they explain much, so I'll use the rings from visualizing addition, subtraction and bitwise complement. `~x + 1`, in terms of such a ring, means "flip it, then draw a CCW arrow on it with a length of one tick". `~(x - 1)` means "draw a CW arrow with a length of one tick, then flip". Picking CCW first is arbitrary, but the point is that the direction is reversed because flipping the ring also flips the arrow if it is drawn first, but not if it is drawn second. Equivalent to drawing an arrow, you may rotate the ring around its center.

So they're equivalent, but why do they negate. The same effect also explains

`a - b = ~(~a + b)`, which when you substitute `a = 0` almost directly gives `-b = ~(b - 1)`. Or using the difference between one's complement and proper negation as I pointed out in that visualization post: the axis of flipping is offset by half a tick, so the effect of flipping introduces a difference of 1 which can be removed by rotating by a tick.

## Bit-string notation

I first saw this notation in The Art of Computer Programming v4A, but it probably predates it. It provides a more "structural" view of negation:
$$-(a10^k) =\; {\sim} (a10^k - 1) =\; {\sim} (a01^k) = ({\sim} a)10^k$$
Here juxtaposition is concatenation, and exponentiation is repetition and is done before concatenation. `a` is an arbitrary bit string that may be infinitely long. It does not really deal with the negation of zero, since the input is presumed to end in 10^{k}, but the negation of zero is not very interesting anyway.

What this notation shows is that negation can be thought of as complementing everything to the left of the rightmost set bit, a property that is frequently useful when working with the rightmost bit. A mask of the rightmost set bit and everything to the right of it can be found with `x ^ (x - 1)` or, on a modern x86 processor, `blsmsk`. That leads to negation by XOR:
$$-x = x\oplus {\sim}\text{blsmsk}(x)$$
which is sort of cheating since `~blsmsk(x) = x ^ ~(x - 1) = x ^ -x`, so this said that `-x = x ^ x ^ -x`.
It may still be useful occasionally, for example when a value of "known odd-ness" is being negated and then XORed with something, the negation can be merged into the XOR.

## Negation by MUX

Using that mask from `blsmsk`, negation can be written as
$$-x = \text{mux}(\text{blsmsk}(x), {\sim} x, x)$$
which combines with bit-level commutativity in some fun ways:

`(~x + 1) + (x - 1) = mux(blsmsk(x), ~x, x) + mux(blsmsk(x), x, ~x) = ~x + x = -1``(~x + 1) | (x - 1) = ~x | x = -1``(~x + 1) ^ (x - 1) = ~x ^ x = -1``(~x + 1) & (x - 1) = ~x & x = 0`

The formula that I've been using as an example for the proof-finder on haroldbot.nl/how.html, `(a & (a ^ a - 1)) | (~a & ~(a ^ a - 1)) == -a`, is actually a negation-by-MUX, written using `mux(m, x, y) = y & m | x & ~m`. The proof haroldbot finds does nothing to explain *why* it is true though.