Quadratic bounds for uncompletable words and matrix mortality
In the authors' words
Every finite nonempty incomplete uniquely decipherable code with maximum word length has an uncompletable word of length at most . 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 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 . A binary partial deterministic family with states has shortest zero product of length , establishing the optimal quadratic order. The bounds and the explicit-code algorithm, including its polynomial work bound, are proved in Lean.
Appeared: Monday, September 28. arXiv. Preprint, not yet peer-reviewed.
Authors' comment: Lean formalization and implementation pilot included as ancillary material