# Zero Padded Basis Representation

## Theorem

Let $b \in \Z: b > 1$.

Let $m \in \Z_{> 0}$.

For every $n \in \Z_{\ge 0}$ such that $n < b^m$, there exists one and only one sequence $\sequence {r_j}_{0 \mathop \le j \mathop \le m - 1}$ such that:

- $(1): \quad \ds n = \sum_{j \mathop = 0}^{m - 1} r_j b^j$
- $(2): \quad \forall j \in \closedint 0 {m - 1}: r_j \in \N_b$

## Informal Proof

The sequence $\sequence {r_j}_{0 \mathop \le j \mathop \le m - 1}$ is the basis representation from the Basis Representation Theorem padded with $0$ to the length of $m$.

## Proof

### Case 1

Let $n \in \Z_{> 0} : n < b^m$.

From Basis Representation Theorem there exists a sequence $\sequence {s_j}_{0 \mathop \le j \mathop \le k}$ such that:

- $(a): \quad \ds n = \sum_{j \mathop = 0}^k s_j b^j$
- $(b): \quad \forall j \in \closedint 0 k: s_j \in \N_b$
- $(c): \quad s_k \ne 0$

First it is shown that:

- $k \le m - 1$

Aiming for a contradiction, suppose:

- $m - 1 < k$

Then:

\(\ds m\) | \(\le\) | \(\ds k\) | ||||||||||||

\(\ds \leadsto \ \ \) | \(\ds b^m\) | \(\le\) | \(\ds b^k\) | Power Function on Integer between Zero and One is Strictly Decreasing | ||||||||||

\(\ds \) | \(\le\) | \(\ds s_k b^k\) | as $s_k > 0$ | |||||||||||

\(\ds \) | \(\le\) | \(\ds \sum_{j \mathop = 0}^k s_j b^j\) | as $b \ge 0$ and $\forall j \in \closedint 0 {k - 1} : s_j \ge 0$ | |||||||||||

\(\ds \) | \(=\) | \(\ds n\) |

This contradicts the premise:

- $n < b^m$

It follows that:

- $k \le m - 1$

Let $\sequence {r_j}_{0 \mathop \le j \mathop \le m - 1}$ be the sequence defined by:

- $r_j = \begin {cases} s_j & : \text{if } j \le k\\ 0 & : \text{if } k < j \le m - 1 \end {cases}$

Then:

\(\ds \sum_{j \mathop = 0}^{m - 1} r_j b^j\) | \(=\) | \(\ds \sum_{j \mathop = 0}^k r_j b^j + \sum_{j \mathop = k + 1}^{m - 1} r_j b^j\) | ||||||||||||

\(\ds \) | \(=\) | \(\ds \sum_{j \mathop = 0}^k s_j b^j + \sum_{j \mathop = k + 1}^{m - 1} 0 \cdot b^j\) | Definition of Sequence $\sequence {r_j}_{0 \mathop \le j \mathop \le m - 1}$ | |||||||||||

\(\ds \) | \(=\) | \(\ds \sum_{j \mathop = 0}^k s_j b^j\) | ||||||||||||

\(\ds \) | \(=\) | \(\ds n\) |

To show that $\sequence {r_j}_{0 \mathop \le j \mathop \le m - 1}$ is unique, let $\sequence {r'_j}_{0 \mathop \le j \mathop \le m - 1}$ be a sequence such that:

- $(1): \quad \ds n = \sum_{j \mathop = 0}^{m - 1} r'_j b^j$
- $(2): \quad \forall j \in \closedint 0 {m - 1}: r'_j \in \N_b$

Since $n > 0$, then:

- $\exists j \in \closedint 0 {m - 1} : r'_j > 0$

Let:

- $k' = \max \set {j : j \in \closedint 0 {m - 1} \text{ and } r'_j > 0}$

Then:

- $(1): \quad \ds n = \sum_{j \mathop = 0}^{k'} r'_j b^j$
- $(2): \quad \ds \forall j \in \closedint 0 {k'}: r'_j \in \N_b$
- $(3): \quad r_{k'} \ne 0$

and

- $(4): \quad \ds \forall j \in \closedint {k + 1} {m - 1}: r'_j = 0$

By definition the sequence $\sequence {r_j}_{0 \mathop \le j \mathop \le k'}$ is a basis representation for $n$.

From Basis Representation Theorem the basis representation for $n$ is unique.

Then:

- $\sequence {r'_j}_{0 \mathop \le j \mathop \le k'} = \sequence {s_j}_{0 \mathop \le j \mathop \le k} = \sequence {r_j}_{0 \mathop \le j \mathop \le k}$

That is:

- $k' = k$

and

- $\forall j \in \closedint 0 k :r'_j = r_j$

It follows that:

- $\forall j \in \closedint {k + 1} {m - 1}: r'_j = 0 = r_j$

So:

- $\forall j \in \closedint 0 {m - 1}: r'_j = r_j$

This establishes that the sequence $\sequence {r_j}_{0 \mathop \le j \mathop \le m - 1}$ is unique.

$\Box$

### Case 2

Let $n = 0$.

Let $\sequence {r_j}_{0 \mathop \le j \mathop \le m - 1}$ be the sequence defined by:

- $\forall j \in \closedint 0 {m - 1} : r_j = 0$.

Then:

- $\ds \sum_{j \mathop = 0}^{m - 1} r_j b^j = \sum_{j \mathop = 0}^{m - 1} 0 \cdot b^j = 0$

This shows that $\sequence {r_j}_{0 \mathop \le j \mathop \le m - 1}$ is a sequence such that:

- $(1): \quad \ds 0 = \sum_{j \mathop = 0}^{m - 1} r_j b^j$
- $(2): \quad \forall j \in \closedint 0 {m - 1}: r_j \in \N_b$

Let $\sequence {r'_j}_{0 \mathop \le j \mathop \le m - 1}$ be a sequence such that:

- $(1): \quad \ds 0 = \sum_{j \mathop = 0}^{m - 1} r'_j b^j$
- $(2): \quad \forall j \in \closedint 0 {m - 1}: r'_j \in \N_b$

Suppose for some $i \in \closedint 0 {m - 1}$, $r'_i > 0$.

Then:

- $\ds \sum_{j \mathop = 0}^{m - 1} r'_j b^j \ge r'_i b^i > 0$.

It follows that:

- $\forall j \in \closedint 0 {m - 1} : r'_j = 0$.

This proves that $0$ has one and only one sequence $\sequence {r_j}_{0 \mathop \le j \mathop \le m - 1}$ such that:

- $(1): \quad \ds 0 = \sum_{j \mathop = 0}^{m - 1} r_j b^j$
- $(2): \quad \forall j \in \closedint 0 {m - 1}: r_j \in \N_b$

$\blacksquare$