A formal approach to twos complement binary representation of integers
Twos complement^{1} is an absolutely great example of modularity. It is a way to represent signed integers in binary format. One of its nice features is that addition and subtraction just works. Twos complement representations can be added and subtracted bit by bit using a carryover bit, without ever having to decode from binary to decimal. It works so well that you basically can forget how the representation works and just remember its properties and how to do certain operations on the binary strings. Up to now I just remembered its “public API” and honestly never cared how the thing works inside. But today I got curious after being confronted with the question how to find the absolute value of a twos complement representation. The algorithm used to compute this is simple:

If the most significant bit is zero the number is positive and can be computed using regular binary conversion

Else:

Flip all the bits of the binary representation

Add one to this new binary number

I mean the positive case makes sense, agreed. But in case of a negative numbers this is seems so random, I wonder how one cannot ask “but why?”. Of course we can look at examples and see that it works. We can come up with some intuition on why it makes sense to do it this way. These approaches are great, but they do not tell us why it works. Only a formal proof can answer this question.
Strict formulation of the problem
In order to present a proof we need a mathematical formulation of the problem. The input is a sequence of bits . We interpret this as the twos complement representation of some integer , using the definition of twos complement:
And the thing we are interested is simply the absolute value of this number in terms of the input .
Proof
We define the flipped input sequence as which is exactly the mirrored sequence of the input. In twos complement this new sequence represents some number . It is not immediately visible what the value of this number is (in terms of s). But summing the two numbers yields the necessary insight:
For a negative number the absolute value is , therefore the algorithm described above is a straight forward application of this result here. The core of the proof is the fact that a bit plus its complement is always one and the formula for partial sums of geometric series^{2}. This equation holds for all integers and is usually the magic behind a some wierd looking twos complement hack or trick.