让下一篇重要论文，不再错过。

原文摘要

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.