Quadratic reset bounds for finite maximal prefix codes
Samrath Singh Chadha
cs.FL
Nov 3, 2026 · v1
TL;DR
All main theorems on reset bounds for prefix-code decoders and the algorithms' polynomial work bounds are formalized in Lean 4 with Mathlib, shipped as ancillary files.
Abstract
Let $C$ be a finite maximal prefix code of maximum codeword length $k\ge2$. We prove that, whenever the literal decoder of $C$ is synchronizing, it has a reset word of length at most $(k-1)(4k-5)$. The bound is independent of the alphabet and the number of decoder states. Its main ingredient is a short-detection theorem: a linear observation of the decoder, with terminal weight constant on states of depth $k-1$, is either identically zero or nonzero on a word of length at most $2k-3$. The proof uses a first-return decomposition in noncommuting variables and cancellation of a highest-degree coefficient. For codes whose codeword lengths are $k-1$ and $k$, we prove the sharper bound $2(k-1)^2-1$ and characterize equality. The binary code with the single short word $a^{k-1}$ attains this bound for every $k\ge2$; an age representation and a potential on circular arcs give the matching lower bound. Both upper bounds yield polynomial-time constructions in the explicit code size. The mathematical results and the algorithms are formalized in Lean, with polynomial work bounds in a specified binary cost model.
Problem
How long can a shortest reset word be for the literal decoder of a synchronizing finite maximal prefix code with maximum codeword length k? The aim is a bound independent of alphabet size and number of decoder states.
Approach
A short-detection theorem shows that a linear observation of the decoder is either identically zero or nonzero on some word of length at most 2k-3. Its proof uses a first-return decomposition in noncommuting variables, embedded in a division ring, plus cancellation of a highest-degree coefficient. This feeds a preimage-expansion argument with cyclic averaging. For codes with two consecutive lengths, a separate parsing-boundary monotonicity argument is used, and a lower bound comes from an age representation and an arc potential. The results and the algorithms are formalized in Lean 4.28.0 with Mathlib, including work bounds in a binary cost model.
Results
Every synchronizing code has a reset word of length at most (k-1)(4k-5). For codes with lengths k-1 and k, the bound is 2(k-1)^2-1, with equality characterized and attained by an explicit binary family. Both constructions run in polynomial time, and all four main results are machine-checked in Lean.
