Quadratic bounds for uncompletable words and matrix mortality
En palabras de los autores
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.
Apareció: lunes, 28 de septiembre. arXiv. Preprint, todavía sin revisión por pares.
Comentario de los autores: Lean formalization and implementation pilot included as ancillary material