Source-linked AI summary
Quadratic bounds for uncompletable words and matrix mortality
Rahul Chandelkar, Samrath Singh Chadha
TL;DR
The paper asks how short an uncompletable word can be when codeword lengths are bounded, independently of the code’s size. It uses path counting and first-return words to construct short witnesses and extend the bound to matrix mortality, with quadratic bounds that are optimal in order.
Problem
How short can the shortest uncompletable word be when every codeword has length at most k, independently of the number of codewords and their total length?
Source: §1 · p. 1Method
The paper uses path matrices and a finite counting identity to find a word with deficient compressed mass, then applies cyclic averaging and padding to obtain an uncompletable word.
Source: §1 · p. 2Results
4k^2-3k bounds the code witness length; 4n^2-3n bounds zero-product length for the stated matrix families, while the binary partial deterministic construction has shortest zero product length k^2+k-1.
Source: §1 · p. 2, §3 · p. 8, §5 · p. 11Takeaways & Limitations
The explicit-code algorithm decides completeness in polynomial time and, for an incomplete code, returns an uncompletable word within the stated bound.
Source: §3 · p. 8For compact matrix input, the first-return code can be exponentially large; the polynomial-time claim concerns explicitly listed codes.
Source: §4 · p. 11
Abstract
from arXiv · showhide
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.
1 Introduction
The paper asks how long the shortest uncompletable word can be when codeword lengths are bounded by k, and proves a quadratic bound with a polynomial-time construction. It also transfers the bound to matrix mortality under a cycle-hub condition.
1 Introduction
- For incomplete codes with maximum word length k, the paper proves a quadratic bound in k for the shortest uncompletable word.The bound is independent of the number of codewords and their total length only if stated in passages? p13 contrasts total length but claim independent is implied; leave out.Source: §1 · p. 1
- A polynomial-time algorithm either certifies completeness or returns an uncompletable word satisfying the bound.The algorithm is given an explicitly listed code and its alphabet.Source: §1 · p. 2
- A mortal matrix family satisfying the joint-spectral-radius and cycle-hub conditions has a zero product of length at most 4n^2 - 3n.The cycle-hub condition means each strongly connected component has a vertex whose deletion leaves an acyclic graph.Source: §1 · p. 2
- A family with 2k - 1 states has shortest zero product of length k^2 + k - 1, establishing the quadratic order for matrix mortality and codes.The lower-bound family is realized through first-return words at a cycle hub.Source: §1 · p. 2
- The code construction uses a finite counting identity and cyclic averaging to find a word of deficient compressed mass, then pads it into an uncompletable word.If a pure codeword ar exists, the method works on its cycle; otherwise, a power of the chosen letter suffices.Source: §1 · p. 2
- Unlike an earlier bound for incomplete codes with deciphering delay, this theorem requires no finite-delay assumption.The earlier result is attributed to Néraud and Selmi.Source: §1 · p. 2
2 The quadratic bound for codes
The code proof represents factors as paths in a flower automaton, compresses path actions to a cycle when a pure codeword exists, and uses deficient mass and padding to obtain an uncompletable word.
2.1 Words as paths
- The flower automaton represents each codeword as a petal from a central vertex, and its labelled paths characterize factors of codeword concatenations.For a code, every entry of each path matrix is 0 or 1.Source: §2.1 · p. 3
2.2 Compression to a cycle
- If no positive power of the chosen letter is a codeword, its power of length 2k−1 is uncompletable; otherwise the pure codeword is unique and has length r ≤ k.In the latter case, long paths labelled only by that letter traverse its pure cycle between an initial suffix and final prefix.Source: §2.2 · pp. 3–4
- Compression acts on the pure cycle’s r coordinates, with r ≤ k, and the padded action agrees there with the compressed word action.The figure identifies the commuting action as (EBwE)L0 = L0Tw.Source: Figure 1 · p. 5, §2.2 · p. 5
2.3 Averaging over cyclic shifts
- Cyclic shifts of a deficient compressed matrix can reduce its mass, while the mass of every compressed word is at most r.Averaging over shifts ensures at least one rotation strictly reduces positive mass.Source: §2.3 · pp. 5–6
2.4 A short deficient word
- Deleting the first complete petal from a sufficiently long path preserves its endpoints and path weight, and incompleteness yields a word of length at most 2k−1 with deficient compressed mass.Recording the deleted codeword makes insertion at the shorter path’s first visit to the central vertex reversible.Source: §2.4 · p. 6
2.5 Padding and the length bound
- Repeatedly inserting suitable cyclic shifts between padded copies of the deficient word reduces the compressed product to zero, and adding end powers makes the resulting word uncompletable.The construction uses at most r copies of the short word, with r ≤ k.Source: §2.5 · pp. 7–8
3 A polynomial-time construction
The algorithm decides completeness and, for an incomplete code, returns an uncompletable word within the quadratic length bound. Finite averaging constructs the word in polynomial time by finding deficient mass and reducing it through rotations.
3 A polynomial-time construction
- Finite averaging selects a short word whose compressed weight is below r, then tests rotations until the mass decreases to zero.Prefix averaging finds a deficient word by choosing each next letter from completion groups whose total weight remains below the threshold.Source: §3 · p. 8
- The algorithm decides completeness in polynomial time and returns an uncompletable word of length at most 4k^2-3k when the code is incomplete.Its running time is polynomial in L and d, with the alphabet represented explicitly.Source: §3 · p. 8
- If all tested prefix counts attain equality, the algorithm certifies completeness; a strict inequality instead supplies the deficient word for the descent.When the code has no power of the chosen letter, the algorithm returns a^{2k-1}.Source: §3 · p. 8
- The descent takes at most r-1 rounds, and its recorded rotations determine an uncompletable output word.A fixed alphabet and rotation order makes the construction deterministic.Source: §3 · pp. 8–9
- The implementation has polynomial bit complexity, with dense arithmetic, bounded rotation tests, and output writing all polynomial in the explicit input parameters.The stated operation bounds include O(kN^2) vector computation, O(r^5) descent tests, and O(k^2) output writing.Source: §3 · p. 9
- For {00, 01, 11, 001}, the algorithm outputs a word of length 11, although a shorter uncompletable word has length 5.The figure illustrates how v = 11 produces a zero product on the two cycle coordinates.Source: §3 · p. 9, Figure 3 · p. 9
4 Matrix mortality
First-return paths at a cycle hub form a finite code under within-component unambiguity. Applying the code bound within components and concatenating their killing words yields a zero product; the reduction allows ambiguity between components.
4 Matrix mortality
- A cyclic component with m vertices and a cycle hub yields a finite first-return code with maximum word length at most m, provided paths with fixed labels and endpoints are unique.First-return paths cannot repeat internal vertices, so their lengths are bounded by m.Source: §4 · p. 10
- Within each cyclic component, the first-return code bound supplies a killing word of length at most 4|D|^2-3|D|.Acyclic components are single vertices without loops and are killed by any letter.Source: §4 · p. 10
- Concatenating component killing words in topological order gives a word whose matrix product is zero.After the final block, no endpoint component remains possible.Source: §4 · p. 10
- The reduction permits ambiguity between different components but requires unambiguity within each component.The within-component condition prevents return paths from amplifying path counts exponentially; for compact matrix input, the first-return code may be exponentially large.Source: §4 · p. 11
5 Matching quadratic lower bounds
The lower-bound construction deletes one unbordered word from all binary words of length k, forcing uncompletable words to cover every alignment. The resulting code and its automaton have shortest witnesses of quadratic length.
5 Matching quadratic lower bounds
- The code X_k = {a, b}^k \ {u}, with u = a^(k−1)b, has U(X_k) = k^2 + k − 1.All words in X_k have the same length, so it is a code.Source: §5 · p. 11
- An uncompletable word must contain u in every alignment, and the selected occurrences cannot overlap, forcing quadratic length.The starts of k such occurrences are at least k + 1 positions apart; W_k = (ua)^(k−1)u attains the bound.Source: §5 · p. 11
- The first-return automaton has 2k − 1 states, is strongly connected, and has q0 as a cycle hub.Removing q0 leaves an acyclic graph; its transition matrices generate a finite monoid.Source: §5 · p. 12, Figure 4 · p. 12
- A word kills this automaton exactly when it is uncompletable for X_k, so its shortest zero product also has length k^2 + k − 1.The missing transition on a^(k−1)b prevents the corresponding path from returning to q0.Source: §5 · p. 12, Figure 4 · p. 12
- For n = 2k − 1 states, the minimum is (n^2 + 4n − 1)/4; these examples establish Θ(n^2) growth, but not the optimal leading constant.For even n ≥ 4, adding an isolated state gives a minimum of at least n^2/4.Source: §5 · p. 12
A An averaging bound for repeated products
This appendix bounds repeated products by averaging integer mass over a finite family of matrices. A strict mass inequality guarantees a zero product, and the result supplies an uncompletable-word bound for codes.
A An averaging bound for repeated products
- If M,T are nonnegative integer matrices and the finite family R_i sums to J, then some sequence of n family members gives the stated repeated-product mass bound.The theorem uses h = |I| and s = μ(T), and applies for every n ≥ 0.Source: A An averaging bound for repeated… · p. 12
- With M = T, the strict inequality s^(n+1) < h^n guarantees a zero product with exactly n inserted family members.A nonzero integer product would have mass at least one, contradicting the inequality.Source: A An averaging bound for repeated… · pp. 12–13
- For a finite code containing a^r, the corollary converts the mass criterion for T_v into an uncompletable-word length bound.The resulting word contains n + 1 copies of v and powers of a; the corollary permits arbitrary |v|.Source: A An averaging bound for repeated… · p. 13
- The strict threshold matters: the example T = R_1 = [1] satisfies the averaging condition, but every product remains.If s = 0, n = 0 already suffices.Source: A An averaging bound for repeated… · p. 13
B Kraft equality and completeness
For finite nonempty codes, Kraft equality implies completeness. The proof uses a bounded integer-valued function on words and extends a maximizing prefix to show no uncompletable continuation can exist.
B Kraft equality and completeness
- A finite nonempty code over an alphabet of size d is complete if its Kraft sum Σ_c d^(−|c|) equals 1.The passage states the implication from Kraft equality to completeness.Source: B Kraft equality and completeness · p. 13
- In the flower automaton, assigning h(q) = d^(k−ℓ(q)) makes Ah = dh, with the root case supplied by Kraft equality.Here ℓ(q) is the remaining petal length to the root.Source: B Kraft equality and completeness · p. 13
- The bounded integer-valued function f(w) attains a positive maximum, and averaging forces every continuation to preserve that maximum.An uncompletable continuation would instead give f(wu) = 0, a contradiction.Source: B Kraft equality and completeness · p. 13
C Formal verification
Lean 4 formalizes the main bounds, lower bounds, and Kraft completeness proof. The code algorithm is verified with a polynomial work bound in a specified arithmetic model.
C Formal verification
- Lean 4 formalizes the proofs of Theorems 1.1, 1.2, and 3.2, the Section 5 lower bounds, and the finite Kraft completeness proof.The development includes the path-deletion bijection and does not assume Kraft completeness as an external result.Source: C Formal verification · p. 14
- The executable algorithm either reports completeness or returns an uncompletable word of length at most 4k^2 − 3k for a uniquely decipherable code.Its input is a list of distinct nonempty codewords over an explicitly given finite alphabet.Source: C Formal verification · p. 14
- The proved work bound is 4174(L + d + 1)^14 in a binary-arithmetic register/array model that charges for operand and index lengths.The bound includes preprocessing and output.Source: C Formal verification · p. 14
- For matrices, Lean constructs component decompositions and first-return codes; the growth-condition equivalence to the norm-limit definition of joint spectral radius is not formalized.The finite-monoid case and lower-bound family for all k ≥ 2 are proved directly.Source: C Formal verification · p. 14
- The proof archive uses Lean 4.19.0 and pinned dependencies, with no admitted proofs or additional axioms beyond the listed standard axioms.The stated axioms are propext, Classical.choice, and Quot.sound.Source: C Formal verification · p. 14
D Implementation pilot
The pilot compares the Lean construction with breadth-first search and a Python reference on 59 dictionaries. Lean completed all five runs on 54 dictionaries, and its median returned-length ratio on the shared matrix-branch sample was 2.5 versus exact breadth-first search.
D Implementation pilot
- The pilot covered 59 distinct dictionaries with maximum word lengths from 1 to 9 and total lengths from 1 to 378.Inputs passed a unique-decipherability check; returned words were checked on the literal flower automaton and completeness by exact Kraft equality.Source: D Implementation pilot · p. 14
- Lean completed all five runs on 54 of 59 dictionaries; on the shared matrix-branch sample, its median returned-length ratio was 2.5 versus exact breadth-first search.Its median construction time also exceeded both references on that sample.Source: D Implementation pilot · p. 14
- Five matrix-branch inputs timed out on every Lean repetition, while both reference methods completed every case.The authors state these implementation-level results establish no asymptotic or application-performance comparison.Source: D Implementation pilot · p. 14