Based on my hazy understanding of the animated GIF file format, I believe that what I ended up with is very similar to animated GIFs, from a high level at least (i.e., a collection of frames, each of which containing multiple rectangles where the frame differs from the previous one). I have no idea why the animated gif encoders I tried did such a poor job size wise, it looked as if none of them even tried to find the minimal set of changes from one frame to another. I didn't spend too long looking, as 8-bit color was always going to be a show stopper.