You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
Status: exploration — speculative, high-effort, genuinely novel if it lands. Pursue in tension with the "keep L9 fast" goals; this is the opposite corner (max ratio, speed no object).
Premise
Zopfli is the de-facto best DEFLATE-compatible ratio, but it is near-optimal, not provably optimal. It approximates the joint optimum of (LZ77 parse, block split, Huffman codes) by:
iterative squeeze: re-running the cost-model optimal parse ~15 times, each iteration pricing symbols with the previous iteration's actual Huffman code lengths — a fixed-point heuristic that can settle in a local minimum or oscillate;
recursive heuristic block splitting (blocksplitter.c) — greedy, not a global optimum over boundaries;
Katajainen length-limited optimal Huffman per block (this part is optimal).
Our L9 is currently a single/double-pass cost-model DP (static round-1 + histogram round-2), i.e. fewer iterations and simpler splitting than zopfli — which is why we are "a bit worse than zopfli" today.
Path: match, then beat
Phase A — match zopfli (prerequisite). Iterative cost-model convergence (feed back real Huffman code lengths, iterate to a fixed point) + better block splitting. Without this, beating zopfli is moot.
Phase B — beat zopfli (each avenue is typically sub-1%, often 0.1-0.5%):
Globally-optimal block splitting via a DP over block boundaries (zopfli's is greedy/recursive). Exact for small inputs, bounded-window approximate for large.
Escape the iteration's local minima: random restarts / annealing on the parse, or a better convergence scheme than zopfli's fixed-point.
Post-pass re-optimization (DeflOpt-style): for the chosen block structure, recompute provably-optimal codes and search local perturbations of block boundaries (merge/split) — known to shave bytes off zopfli output.
Exact-cost DP: price candidates inside the DP with the real final code lengths rather than an estimate. Zopfli never does this (its per-iteration cost is an approximation). This is our structural advantage — see below.
Our unique angle
We already have a verified, exact bit-cost model and DP infrastructure (DeflateParse.lean, BlockSizeModel.lean). A DP that prices with the exact cost model — rather than zopfli's previous-iteration estimate — is the theoretical improvement, and we are unusually well placed to build it correctly. The payoff framing: a formally-verified encoder that beats the best-known DEFLATE ratio would be a genuinely novel result, not just a re-implementation.
Magnitude / risk
Realistic gains over zopfli are small (sub-1% on real corpora) at large compute cost (zopfli is already ~100x zlib; this is more).
Context: requested explicitly — "is there any possibility of getting even better compression than zopfli?" Yes, within DEFLATE: zopfli is near-optimal, not optimal, and the avenues above are real, though the gains are small and the cost is high.
Status: exploration — speculative, high-effort, genuinely novel if it lands. Pursue in tension with the "keep L9 fast" goals; this is the opposite corner (max ratio, speed no object).
Premise
Zopfli is the de-facto best DEFLATE-compatible ratio, but it is near-optimal, not provably optimal. It approximates the joint optimum of (LZ77 parse, block split, Huffman codes) by:
blocksplitter.c) — greedy, not a global optimum over boundaries;Our L9 is currently a single/double-pass cost-model DP (static round-1 + histogram round-2), i.e. fewer iterations and simpler splitting than zopfli — which is why we are "a bit worse than zopfli" today.
Path: match, then beat
Phase A — match zopfli (prerequisite). Iterative cost-model convergence (feed back real Huffman code lengths, iterate to a fixed point) + better block splitting. Without this, beating zopfli is moot.
Phase B — beat zopfli (each avenue is typically sub-1%, often 0.1-0.5%):
Our unique angle
We already have a verified, exact bit-cost model and DP infrastructure (
DeflateParse.lean,BlockSizeModel.lean). A DP that prices with the exact cost model — rather than zopfli's previous-iteration estimate — is the theoretical improvement, and we are unusually well placed to build it correctly. The payoff framing: a formally-verified encoder that beats the best-known DEFLATE ratio would be a genuinely novel result, not just a re-implementation.Magnitude / risk
Relationship
Context: requested explicitly — "is there any possibility of getting even better compression than zopfli?" Yes, within DEFLATE: zopfli is near-optimal, not optimal, and the avenues above are real, though the gains are small and the cost is high.