Quadratic bounds for uncompletable words and matrix mortality
Rahul Chandelkar, Samrath Singh Chadha
cs.FL
Sep 25, 2026 · v2
math.CO
TL;DR
The quadratic bounds for uncompletable words and matrix mortality, together with the explicit-code algorithm and its polynomial work bound, are proved in Lean.
Abstract
Every finite nonempty incomplete uniquely decipherable code with maximum word length $k$ has an uncompletable word of length at most $4k^2-3k$. The bound is independent of the number of codewords and their total length. Deleting a complete codeword cycle gives a finite path-counting identity; Kraft equality then supplies a short word of deficient compressed mass. Cyclic averaging and padding turn it into an uncompletable word. Conditional expectation makes the construction polynomial-time and also decides completeness. First-return words extend the bound to mortal families of nonnegative integer $n\times n$ matrices with joint spectral radius at most one, provided every strongly connected component has a vertex meeting every cycle. Such a family has a zero product of length at most $4n^2-3n$. A binary partial deterministic family with $2k-1$ states has shortest zero product of length $k^2+k-1$, establishing the optimal quadratic order. The bounds and the explicit-code algorithm, including its polynomial work bound, are proved in Lean.
Problem
How long can the shortest uncompletable word of a finite incomplete uniquely decipherable code be, as a function of its maximum codeword length k? A related question asks for the shortest zero product in a mortal family of nonnegative integer matrices.
Approach
Paths in the flower automaton are reduced to matrices of size at most k. Deleting a complete codeword cycle and applying Kraft equality yields a short word of deficient mass. Cyclic averaging and padding turn it into an uncompletable word, and conditional-expectation (prefix averaging) arguments make the construction polynomial-time. First-return codes at a cycle hub extend the result to matrix families with joint spectral radius at most one; the results are proved in Lean.
Results
Every such code has an uncompletable word of length at most 4k^2-3k, and a polynomial-time algorithm decides completeness. Under the cycle-hub condition, a mortal matrix family has a zero product of length at most 4n^2-3n. A binary automaton with 2k-1 states has shortest zero product of length k^2+k-1, showing the quadratic order is optimal.
