Ideal-real interval coding is prefix-free and lossless

At every prefix, the $m$ child intervals are disjoint half-open intervals whose union is the parent interval, because the cumulative probabilities increase from $0$ to $1$. Induction on prefix length therefore shows that the length-$n$ intervals partition $[0,1)$, and multiplying the successive width factors gives $\mathrm{\mid }I(x^n)\mathrm{\mid }=p^n(x^n)>0$ by [F1].

By [F8], put $w=\mathrm{\mid }I(x^n)\mathrm{\mid }$ and $r=\lfloor -{\log }_{2}w\rfloor$. Since $0<w\le 1$, [F4] and [F5] give $-{\log }_{2}w\ge 0$, so [F7] gives $r\ge 0$ and $r\le -{\log }_{2}w<r+1$. The same facts show that ${\log }_2$ is strictly increasing, and [F6] gives ${\log }_2(2^u)=u$; therefore $2^{-(r+1)}<w\le 2^{-r}$. Thus the cell width $\delta :=2^{-(r+2)}$ satisfies $\delta <w\mathrm{/}2$. If $c$ is the midpoint of $I(x^n)$, then $0\le c<1$ by step 1.1. By [F7], $k=\lfloor 2^{s}c\rfloor$ is an integer; since $0\le c<1$, it satisfies $0\le k<2^s$ and has an $s$-bit representation. Its cell $[k\delta ,(k+1)\delta )$ contains $c$ and lies within distance $\delta$ of it; hence it is contained in the interior of $I(x^n)$.

Distinct blocks have disjoint source intervals by step 1.1. Their nonempty dyadic cells from step 2.1 are therefore disjoint. If one emitted bit word were a prefix of another, its dyadic cell would contain the other's cell, contradicting disjointness. Thus the codewords are distinct and prefix-free by [F3]; the unique interval containing a received code cell identifies its block, and prefix-freeness parses concatenated fixed-$n$ frames.

By [F7] and [F8], $r\le -{\log }_{2}w$, so the emitted length is $s=r+2\le -{\log }_{2}w+2=-{\log }_2{p}^n(x^n)+2$ by step 1.1 and [F1]. This proves the pointwise bound without converting ideal-real interval arithmetic into a finite-register procedure.