The rational finite-register arithmetic code is prefix-free and lossless

After $t$ symbols, the scaled interval for the prefix is $[L,L+W{Q}^{n-t})$. At $t=0$ it is $[0,Q^n)$, so the claim holds. If it holds at $t-1$, symbol $i$ occupies the subinterval beginning $W{c}_i{Q}^{n-t}$ after the parent lower endpoint and of width $W{q}_i{Q}^{n-t}$; the widths sum to the parent width because ${\sum }_i{q}_i=Q$. Thus the update [F3] gives the claimed child interval. At $t=n$ it is $[L,L+W)$ with $W={\prod }_{t=1}^n{q}_{x_t}$, so after division by $D=Q^n$ its width is $W\mathrm{/}D=p^n(x^n)>0$ by [F1].

The search in [F3] finds $u$ with $2^{u}W\le D<2^{u+1}W$: $j=0$ is admissible since $W\le Q^n$, and $D\mathrm{/}W\le Q^n\le 2^B$, so the largest admissible $u$ is at most $B$. Hence $2^{-(u+1)}<W\mathrm{/}D\le 2^{-u}$. The selected dyadic cell has width $\delta =2^{-(u+2)}<W\mathrm{/}(2D)$. Its index $k$ is the floor of $2^s$ times the interval midpoint $(2L+W)\mathrm{/}(2D)$; therefore the cell contains that midpoint and extends by at most $\delta$ to either side. Since $\delta$ is smaller than half the source-interval width, the cell lies inside the source interval. Also the midpoint is in $[0,1)$, so [F7] gives $0\le k<2^s$ and its $s$-bit representation exists.

Length-$n$ source intervals partition $[0,1)$ by step 1.1, and step 2.1 places each nonempty emitted dyadic cell inside its own interval. Thus cells for distinct blocks are disjoint. A proper-prefix relation between emitted words would make one dyadic cell contain the other, which contradicts disjointness. The codewords are distinct and prefix-free by [F2]. A trie leaf therefore identifies one block, so the decoder returns exactly the encoded block.

Since $2^u\le D\mathrm{/}W$, [F4], [F5], and [F6] give $u={\log }_2(2^u)\le {\log }_2(D\mathrm{/}W)$; [F4] and [F8] give ${\log }_2(D\mathrm{/}W)=-{\log }_2(W\mathrm{/}D)=-{\log }_2{p}^n(x^n)$ by step 1.1. Thus the payload length $s=u+2$ is at most $-{\log }_2{p}^n(x^n)+2$. Also $W\ge 1$ and $D\le Q^N\le 2^B$, so $u\le B$ and $s\le B+2$. At configuration, computing $P=Q^N$ takes $N$ multiplications. The doubling loop for $B$ terminates because $2^P\ge P$ for every positive integer $P$ (by induction), and its first $B$ with $2^B\ge P$ is least. The encoder performs $n$ updates, tests at most $B+1$ values of $j$, and emits at most $B+2$ bits; the decoder's trie traversal reads at most that many bits and outputs $n$ symbols. Since $N\ge 1$, $Q\le Q^N\le 2^B$, so each $q_i$ and $c_i$ fits its $B+1$-bit register; also $L,W,D\le 2^B$, so their $B+1$-bit registers suffice. By [F9], if $b_N=\lceil {\log }_2(N+1)\rceil$ and $b_B=\lceil {\log }_2(B+3)\rceil$, then $b_N\ge {\log }_2(N+1)$ and $b_B\ge {\log }_2(B+3)$. Applying the increasing logarithm facts [F4]–[F6] gives $2^{b_N}\ge N+1$ and $2^{b_B}\ge B+3$, so the counters hold counts up to $N$ and output lengths up to $B+2$. By [F10], the numerator $2^s(2L+W)$ is at most $2^{B+2}\cdot 3\cdot 2^B<2^{2B+4}$, so the temporary register suffices; the denominator $2D$ and scale $2^s$ also fit it. All other products in the interval update are at most $D$. Hence every loop terminates and no configured per-frame register overflows.