Succinct: SOLE: proof

fs-succinct/succinct.tex

@@ -187,11 +187,20 @@ on a RAM, so we can do constant-time arithmetic on the blocks.
 Note that this representation is locally decodable and modifiable -- each input
 block affects at most 4 output blocks.
 
-
 Now we must check that all the alphabet transformations are valid, i.e., the
 output universe of each transformation is always at least as big as the input
 universe.
 
+For the first pass, we want:
+$$\eqalign{
+(B+1)^2      &\le (B-3i)(B+3i+3)\cr
+B^2 + 2B + 1 &\le B^2 + 3B - 9i^2 - 9i\cr
+B            &\ge 9i^2 + 9i + 1\cr
+}$$
+We know $B \ge 4n^2$ and $i \le {n+1\over 2}$. By plugging $i = {n+1\over 2}$
+and doing some algebraic manipulation, we can verify that the inequality holds.
+
+For the second pass, this is trivial, as $(B+i)(B-i) = B^2 - i^2 \le B^2$.
 
 
 \section{Succinct representation of arbitrary-alphabet strings}