Non adjacent form of an integer is unique I have tried to look up the proof for NAF (Non-adjacent form) being unique for every integer, but as far as I have seen, textbooks only mention it as a property of NAF, but no proof is given. Also I understand that the number of zeroes in NAF representation is more than in its binary representation but how do I prove that NAF representation of an integer has 2k/3 zeroes for a k-bit integer in general. Even a textbook reference that contains these proofs would be appreciated.
Non-Adjacent Form (NAF), also called Balanced Binary Representation (BBR), is a representation of integers reminiscent of binary, but with an extra $-1$ value for digits, and such that at least one of two adjacent digits is $0$. Because the resulting representation has at least half of its digits at zero (typically about $2/3$), it can be used to speed-up modular exponentiation, or point multiplication on an arbitrary group (e.g. Elliptic Curve).



We define a NAF of $a\in\mathbb N$ as any tuple of $j\in\mathbb N$ integers $a_i\in\{-1,0,+1\}$ with $0\le i&lt;j$, such that:


$a=\sum_{i=0}^{i=j-1}a_j\;2^j\;\;$ (same formula as for binary)
$j&gt;0\implies a_{j-1}\ne0\;\;$ (the highest-rank digit, if any, is non-zero)
$0&lt;i&lt;j\implies a_i\;a_{i-1}=0\;\;$ (at least one of two adjacent digits is $0$)


Each $a$ has a unique NAF (we'll prove this in detail). These defining properties of NAF need no change for an extension to $a\in\mathbb Z$. There is either $0$ or $1$ more digit in the NAF for $a$ than in the binary representation of $|a|$; more precisely, for $a\ne0$, $j=\lceil\log_2(3|a|)\rceil-1$.

Counting from $0$ in NAF goes (showing the big-endian form, then the little-endian tuple):
 $\;a=0:\;$             $\;\;\;j=0\;\;()$
 $\;a=1:\;$          +1 $\;\;\;j=1\;\;(a_0=+1)$
 $\;a=2:\;$       +1  0 $\;\;\;j=2\;\;(a_0=\;\;\;0,\;a_1=+1)$
 $\;a=3:\;$    +1  0 -1 $\;\;\;j=3\;\;(a_0=-1,\;a_1=\;\;\;0,\;a_2=+1)$
 $\;a=4:\;$    +1  0  0 $\;\;\;j=3\;\;(a_0=\;\;\;0,\;a_1=\;\;\;0,\;a_2=+1)$
 $\;a=5:\;$    +1  0 +1 $\;\;\;j=3\;\;(a_0=+1,\;a_1=\;\;\;0,\;a_2=+1)$
 $\;a=6:\;$ +1  0 -1  0 $\;\;\;j=4\;\;(a_0=\;\;\;0,\;a_1=-1,\;a_2=\;\;\;0,\;a_3=+1)$
 $\;a=7:\;$ +1  0  0 -1 $\;\;\;j=4\;\;(a_0=-1,\;a_1=\;\;\;0,\;a_2=\;\;\;0,\;a_3=+1)$
 $\;a=8:\;$ +1  0  0  0 $\;\;\;j=4\;\;(a_0=\;\;\;0,\;a_1=\;\;\;0,\;a_2=\;\;\;0,\;a_3=+1)$
 $\;a=9:\;$ +1  0  0 +1 $\;\;\;j=4\;\;(a_0=+1,\;a_1=\;\;\;0,\;a_2=\;\;\;0,\;a_3=+1)$



To establish that an integer $a$ can't have two different NAFs, we use an argument of infinite descent, a special case of proof by contradiction. We hypothesize there exists integer(s) with at least two distinct NAFs, and define $a$ as the smallest such integer. We'll construct an integer $b$ less than $a$ with two distinct NAFs (leading to contradiction).

We note one of the two distinct NAFs for $a$ using $j$ and $a_i$, and another using $\tilde j$ and $\tilde a_i$, swapping theses if necessary so that $\tilde j\le j$. The only case with $j=0$ gives both NAF empty, thus identical, hence $j\ge1$.

If we had $a=0$, we would have $a=0=\sum_{i=0}^{i=j-1}a_j\;2^j$ with $a_{j-1}\ne0$, and by explicitly computing the minimum and maximum of the other terms as a sum-of-powers, we show this can't hold. Hence $a&gt;0$, and hence $\tilde j\ge1$.

We consider three cases each leading to contradiction:


If $a\equiv0\pmod2$, then by reducing modulo $2$ the equation $a=\sum a_i\;2^i$, it comes that $a_0=0$.
$b=a/2$ is an integer less than $a$ (since $2b=a$ with $a&gt;0$), and it's easily verified that the $j-1$ integers $b_i=a_{i+1}$ for $0\le i&lt;j-1$ obey each condition for a NAF for that $b$. Similarly, a NAF for that $b$ is the $\tilde j-1$ integers $\tilde b_i=\tilde a_{i+1}$ for $0\le i&lt;\tilde j-1$, and that's another NAF (since $a_0=0=\tilde a_0$ and the two NAFs for $a$ are distinct).
If $a\equiv1\pmod4$, then by reducing modulo $4$ the equation $a=\sum a_i\;2^i$, it comes that $2a_1+a_0\equiv1\pmod4$, thus $a_1=0$ and $a_0=+1$ (notice that $a_1=+1$ and $a_0=-1$ is ruled out by $a_1\;a_0=0$).
$b=a-1$ is an integer less than $a$, and a NAF for that $b$ is the $j$ integers $b_0=0$, and $b_i=a_i$ for $1\le i&lt;j$. Similarly, another NAF for that $b$ is the $\tilde j$ integers $\tilde b_0=0$, and $\tilde b_i=\tilde a_i$ for $1\le i&lt;\tilde j$.
If $a\equiv3\pmod4$, then by reducing modulo $4$ the equation $a=\sum a_i\;2^i$, it comes that $2a_1+a_0\equiv3\pmod4$, thus $a_1=0$ and $a_0=-1$ (notice that $a_1=-1$ and $a_0=+1$ is ruled out by $a_1\;a_0=0$).
$b=(a+1)/2$ is an integer less than $a$, and a NAF for that $b$ is the $j-1$ integers $b_i=a_{i+1}$ for $0\le i&lt;j-1$. Similarly, another NAF for that $b$ is the $\tilde j-1$ integers $\tilde b_i=\tilde a_{i+1}$ for $0\le i&lt;\tilde j-1$.




There are several ways to explicitly construct the NAF of an arbitrary integer $a&gt;0$ from that of a smaller integer $b$, recursively, until reaching $b=0$ that has a trivial NAF. For example:


If $a\equiv0\pmod2$, we build the NAF for $a$ as a tuple with one more element than the NAF of $b=a/2$, with $a_0=0$, $a_{i+1}=b_i$.
If $a\equiv1\pmod4$, we build the NAF for $a$ as a tuple with two more elements than the NAF of $b=(a-1)/4$, with $a_0=+1$, $a_1=0$, $a_{i+2}=b_i$.
If $a\equiv3\pmod4$, we build the NAF for $a$ as a tuple with two more elements than the NAF of $b=(a+1)/4$, with $a_0=-1$, $a_1=0$, $a_{i+2}=b_i$.


In all three case, it is easy to derive the properties required from the NAF of $a$ from these for the NAF of $b$.



Various sources credit the idea, proof of uniqueness of NAF representation, and proof of optimality of the non-adjacency criteria from the standpoint of maximizing the number of zeros, toGeorge W. Reitwiesner, Binary arithmetic (paywalled), Advances in Computers, vol. 1, pp. 231-308, 1960.

I recommend Jeffrey Shallit: A Primer on Balanced Binary Representations (1992-1993, Department of Computer Science, University of Waterloo). I'm not the only one to find it late!

Marc Joye and Christophe Tymen: Compact Encoding of Non-Adjacent Forms with Applications to Elliptic Curve Cryptography (in proceedings of Public Key Cryptography 2001) notice that we can re-encode NAF as bits using a simple Hamming code, storing integers as NAF essentially as compactly as in binary, while keeping them directly usable for fast point multiplication.