M₃(5): Mortality of Five 3 × 3 Integer Matrices

Known Stuff#

An undecidability proof for matrix mortality converts halting in three stages: a halting computation becomes an equality of two words, the word equality becomes a zero matrix entry, and the zero entry becomes a zero matrix product. Each stage must also preserve failure: a nonhalting computation must produce no word equality, and no product may vanish unless some word equality holds.

Bounds before this work#

For dimension d and generator bound k, undecidability of M_d(k) is monotone in both parameters: extra generators may go unused, and A ↦ A ⊕ 0 preserves mortality. The minimal undecidable cells therefore form an antichain. Before this work the best published antichain was [Cassaigne et al. 2014]

M_{3} (6), M_{5} (4), M_{9} (3), M_{15} (2) .

Its first entry comes from Neary’s five-pair PCP: five word-pair matrices and one separator [Neary 2015].

Generator packing#

Cassaigne et al. also proved the packing reduction

M_{d} (h k + 1) \leq_{m} M_{k d} (h + 1),

where ≤_m denotes a computable many-one reduction [Cassaigne et al. 2014]. It trades generators for dimension. Each original generator is spelled as a codeword of a prefix code over fewer letters, and the matrices keep one d-dimensional block for each unfinished prefix, so that a product can remember how much of a codeword it has read. For five generators, the ternary code 0, 1, 20, 21, 22 has two unfinished prefixes and gives dimension 2d; the binary code 0, 10, 110, 1110, 1111 has four and gives dimension 4d. The converse must handle products that begin in the middle of a codeword; a synchronizing word does this, as the binary compilers show in detail for a different five-leaf code.

Tag systems#

A tag system with deletion width β stores a word, its queue. A step reads the first letter of the queue, appends the word assigned to that letter, and deletes the first β letters. The system halts when fewer than β letters remain.

Neary’s binary tag systems use the letters b and c, a width β ≥ 3, and a word B over b, c, called the body:

b \mapsto b, c \mapsto B b, I = (B without its first β - 1 letters) b .

Here I is the initial queue. Neary compiles every program and input into such a pair (β, B), so halting from I is undecidable [Neary 2015]. The compiler has a free padding parameter; choosing it as in the padding note below also makes β−1 divide |B|, which the proof here uses.

Record a run by its strokes, the blocks of β letters deleted by successive steps. Every letter ever present is either deleted by some stroke or still in the queue, so after any number of steps

(strokes) (current queue) = I (appended words) .

This history identity is the standard bridge from tag systems to correspondence problems: one side of a word equation spells the strokes, the other spells the appended words, and a solution certifies a run.

Correspondence with a fixed boundary#

A Post correspondence instance PCP(n) has n word pairs (u_i, v_i) and asks for a nonempty index word w with u(w) = v(w), where u(w) and v(w) are the concatenated upper and lower words. The generalized problem GPCP(n) also fixes boundary words that must appear once, at the ends [Nicolas 2008]. The instance in this article has empty left boundaries, the upper right boundary M, and an empty lower right boundary, so it asks whether

\exists w : U (w) M = V (w) .

The empty word is not a solution, because M is nonempty.

The terminal-pair problem#

Neary’s four simulation pairs finish a halting run with a leftover: the equation they satisfy is U(w)M = V(w), not U(w) = V(w). Ordinary PCP therefore needs a selectable pair that supplies M, and such a pair can also be selected too early or more than once. The converse must exclude every such misuse.

Neary’s 2013 report made one erasing pair serve both for simulation and for termination and claimed PCP(4) and M₃(5) [Neary 2013]; the exclusion of misuse at arbitrary positions was not established there, and the refereed successor proved PCP(5) with a separate terminal pair and left PCP(4) open [Neary 2015]. Rote later found an error in that terminal pair’s guard and proposed a longer replacement [Rote 2025]. Neither terminal pair is used here.

From word equations to mortality#

Matrices can accumulate numerical codes of two words, but equality of the words is then a single zero entry, not a zero matrix. Two standard constructions close the gap: a matrix representation of word pairs, and a rank-one matrix that turns one zero entry into a zero product.

Word-pair matrices#

Recode the binary digits 0 and 1 as the ternary digits 1 and 2, and let σ(x) be the base-three value of the recoded word x. Because no digit is 0, σ is injective on all words, including words of different lengths. Concatenation shifts the first numeral by the length of the second:

σ (xy) = σ (x) 3^{| y |} + σ (y) .

The matrix

Ψ (x, y) = [\begin{matrix} 1 & σ (y) & σ (x) - σ (y) \\ 0 & 3^{| y |} & 3^{| x |} - 3^{| y |} \\ 0 & 0 & 3^{| x |} \end{matrix}]

applies this shift to both words at once and keeps their difference in the upper-right entry [Cassaigne et al. 2014]. With e₁, e₃ the first and third coordinate columns, direct multiplication gives:

Concatenation

Ψ (x x^{'}, y y^{'}) = Ψ (x, y) Ψ (x^{'}, y^{'})

Equality test

e_{1}^{T} Ψ (x, y) e_{3} = 0 \Leftrightarrow x = y

Nonsingularity

\det Ψ (x, y) = 3^{| x | + | y |} \neq 0

For a family of pairs (u_a, v_a), put X_a = Ψ(u_a, v_a) and write X_w for the product along an index word w. Then X_w = Ψ(u(w), v(w)).

The rank-one separator#

A right boundary pair (s, t) is absorbed into a column rather than added as a selectable pair. Put X_★ = Ψ(s, t) and

c = X_{★} e_{3}, A_{★} = c e_{1}^{T} .

By the concatenation law, e₁^TX_wc = e₁^TΨ(u(w)s, v(w)t)e₃, which vanishes exactly when u(w)s = v(w)t. The rank-one separator A_★ turns that scalar into a matrix: for a solution w,

A_{★} X_{w} A_{★} = c (e_{1}^{T} X_{w} c) e_{1}^{T} = 0 .

One generator supplies both rank-one factors.

Arbitrary products#

Mortality quantifies over every product, so the converse must show that no other product vanishes. A product without A_★ is nonsingular. A product with r ≥ 1 copies of A_★ has a unique form

Q_{0} A_{★} Q_{1} A_{★} \dots A_{★} Q_{r},

where each Q_j is a possibly empty product of ordinary generators. Regrouping the rank-one factors gives

(Q_{0} c) [\prod_{1 \leq j < r} e_{1}^{T} Q_{j} c] (e_{1}^{T} Q_{r}) .

The outer column and row are nonzero because the Q_j are nonsingular and c, e₁ are nonzero. The product is therefore zero exactly when r ≥ 2 and some inner scalar e₁^TQ_jc is zero, that is, when some index word solves the boundary equation. This is Halava, Harju, and Hirvensalo’s endpoint absorption [Halava–Harju–Hirvensalo 2007]:

Fixed-boundary compiler

For a finite alphabet α, maps u, v: α → {0,1}^*, and right boundaries s, t,

{X_{a} : a \in α} \cup {A_{★}} is mortal \Leftrightarrow \exists w \in α^{*} : u (w) s = v (w) t .

The family has |α| nonsingular upper-triangular generators and one rank-one generator, all 3 × 3. A GPCP instance with n pairs and one right boundary pair therefore costs n + 1 generators, the same as an ordinary PCP(n) instance.

New Stuff#

Result#

The fixed-boundary compiler charges one generator for the boundary whether or not the boundary is a selectable pair. Neary’s four simulation pairs already end every halting run with the fixed leftover M, so treating M as a boundary word gives a four-pair GPCP instance and hence four ordinary generators plus one separator. The terminal-pair problem disappears, because a boundary word occurs exactly once, at the end, by definition. What remains is the converse for arbitrary tile words: a word that follows no computation must not satisfy the equation. The proof below derives it from one global identity instead of analyzing local mistakes.

Theorem (fixed-boundary correspondence). Let β ≥ 3, and let the body B satisfy |B| ≥ β−1 and β−1 ∣ |B|. For the four tiles defined below,

\exists w : U (w) M = V (w) \Leftrightarrow the tag system halts from I .

Hence GPCP(4) over a binary alphabet is undecidable.

Theorem (M₃(5)). A primitive-recursive map sends every program to five 3 × 3 integer matrices, four nonsingular and upper triangular and one of rank one, that are mortal exactly when the program halts. Hence M₃(5) is undecidable.

Packing with 5 = 2·2 + 1 and 5 = 1·4 + 1 gives M₆(3) and M₁₂(2); padding gives the other consequences in the abstract. Later results in this series lower several of these cells; the decidability table records the current state.

Four tiles#

Encode queue letters, and define the boundary word, by

H (b) = 1 0^{β} 1, H (c) = 1, M = 1 0^{β} .

Thus M is H(b) without its final 1. Extend H to words by concatenation. The four tiles are Neary’s simulation pairs:

Tile	Upper word	Lower word	Role
R_c	1	1 H(B) 1 0	read c, append `B`b
R_b	1 0^β 1	1 1 0	read b, append b
D_c	1	0	delete one c
D_b	1 0^β 1	0	delete one b

For a tile word w, U(w) and V(w) are its upper and lower concatenations. A tag step is simulated by a block of one rule tile R_x followed by β−1 deletion tiles, which together read one stroke. The upper side spells H of the letters read. The lower side spells H of the appended words, one letter ahead: it begins with H(c) = 1, and the final 1 of each appended b is written by the next rule tile. After each complete block with current queue q,

V (w) 1 = U (w) H (q) .

This is the history identity in encoded form. A halted queue is b, and H(b) = M1, so the identity at halting is U(w)M = V(w). The first block performs a virtual step from the one-letter queue c: it appends Bb and deletes c together with the first β−1 letters of B, leaving exactly I.

Padding into the arithmetic envelope

If the cyclic program has p appendants, Neary’s construction has β = 10p and |Bb| = βs, where s is a padding length. If n is the input length and r the maximum cyclic appendant length, take

N = \max {11 (n + p) + β - 2, 11 p, 11 r, 1}, x = ⌈ \frac{N - 1}{β - 1} ⌉, s = x (β - 1) + 1 .

This choice makes every variable exponent in Neary’s Table 2 nonnegative, so every specified track still has length s. Increasing s changes only the padding and the number of full copies of the program word. That word has length βs, so extra copies do not change the length and shift residues modulo β that Neary’s track-by-track simulation uses, and Table 2 remains valid. Moreover,

| B | = β [x (β - 1) + 1] - 1 = (x β + 1) (β - 1),

so β−1 ∣ |B| and |B| ≥ β−1.

A worked run#

Take β = 3 and B = cbcb, so I = cbb. The run halts after five steps, and its solution is the 18-tile word formed by the six blocks below, the first being the virtual step.

Block	Stroke deleted	Word appended	Queue afterwards
R_c D_c D_b	ccb	cbcbb	cbb
R_c D_b D_b	cbb	cbcbb	cbcbb
R_c D_b D_c	cbc	cbcbb	bbcbcbb
R_b D_b D_c	bbc	b	bcbbb
R_b D_c D_b	bcb	b	bbb
R_b D_b D_b	bbb	b	b

Both sides of U(w)M = V(w) have 66 binary letters. After the virtual step, the strokes followed by the final queue spell cbbcbcbbcbcbbbbb, which is also I followed by the appended words.

Soundness: every solution is a halting run#

Assume U(w)M = V(w) for an arbitrary tile word w.

Synchronization

The upper side is an H-encoded word followed by M, so every maximal run of zeros in it has length exactly β. On the lower side a rule tile ends with one zero, each deletion tile adds one more, and the next rule tile begins with a one. The payload H(B) contains only complete runs of β zeros and ends at a codeword boundary before the rule tile’s final 10. Hence every rule tile is followed by exactly β−1 deletion tiles, and w factors into blocks

R_{a_{0}} D_{a_{1}} \dots D_{a_{β - 1}},

one for each stroke a₀⋯a_β−1. This scan reads the word itself; it does not assume that w begins with a simulated history.

History equation

Appending a final 1 to both sides turns M into H(b), and H is injective, so the equation decodes to an equation between letter words. It forces the first stroke to be cz with z the first β−1 letters of B; here |B| ≥ β−1 is used. Cancel this virtual step. For the remaining strokes S, let C(S) be their concatenation and P(S) the concatenation of the words appended for their first letters. The equation becomes

C (S) b = I P (S),

the history identity with final queue b.

Execution

Suppose the current queue has at least β letters. It and the next stroke are both prefixes of the same side of the equation, and the stroke has length β, so the stroke is the first β letters of the queue: the block performs the genuine tag step. Delete the stroke, append the word selected by its first letter, cancel the common prefix, and repeat. When the queue has fewer than β letters, the tag system has halted, and any unused remainder of the equation is irrelevant.

More generally, for any tag system of width β, an equation C(S)F = IP(S) with |F| < β implies halting from I. Correctness of a new tile set then reduces to forcing blocks and decoding its equation into this form.

No step examines a local mistake: synchronization fixes the block structure of every word, and the history equation alone forces each block to be the correct step.

Completeness: every halting run is a solution#

Every reachable queue ends in b and has length congruent to 1 modulo β−1, because I does and each step appends |B| + 1 or 1 letters and deletes β; here β−1 ∣ |B| is used. A queue shorter than β is therefore exactly b. Writing the virtual step and each tag step as its block gives a tile word that satisfies the encoded history identity with q = b, which is U(w)M = V(w).

Corollary: a corrected five-pair PCP#

Adjoin a fresh letter # and the pair

(M #, #) .

Every tile’s upper word ends in 1 and every lower word ends in 0, so no word of tiles alone solves PCP. At the first occurrence of the new pair, prefix compatibility of U(w)M# and V(w)# forces U(w)M = V(w), and the prefix through that pair is already a solution. A primitive solution, one that is not the concatenation of two nonempty solutions, therefore uses the new pair exactly once and last. The fixed-length code 0 ↦ 00, 1 ↦ 01, # ↦ 11 returns to a binary alphabet and preserves equality, prefix comparability, and primitivity. This gives five-pair PCP without Neary’s terminal pair.

The same argument reduces any fixed-boundary equation U(w)s = V(w)t whose ordinary pairs have no PCP solution to PCP with the additional pair (s#, t#).

Five matrices#

Apply the fixed-boundary compiler to the four tiles with s = M and t empty. The ordinary generators are X_a = Ψ(u_a, v_a) for the tiles a, and the separator is A_★ = ce₁^T with

c = Ψ (M, ε) e_{3} = {(σ (M), 3^{| M |} - 1, 3^{| M |})}^{T},

where ε is the empty word. The five matrices have integer entries; the four tile matrices are nonsingular and upper triangular, and A_★ is nonzero of rank one. By the compiler and the correspondence theorem, the family is mortal exactly when the tag system halts. The maps from programs to Neary’s (β, B) and from (β, B) to the five matrices are primitive recursive, so this is a many-one reduction from the halting problem.

Bookkeeping#

Verification and provenance#

Formalized reduction

Lean checks the universal halting reduction, the tile synchronization theorem, queue-history soundness (tagHaltsFrom_of_history), the corrected five-pair PCP, the word-pair representation, the fixed-boundary compiler (absorbedFamilyInt_mortal_iff_terminal_match), the converse for every product of the five matrices, and the final theorems UniversalNeary.codeHalts_reduces_mortality35 and UniversalNeary.mortality35_not_computable.

Computable source reduction

Lean proves a primitive-recursive many-one reduction from mathlib’s code-halting predicate, through a fixed universal machine and Neary’s compiler, to the five-matrix family. Neary’s undecidability lemma is provenance, not a premise of the formal proof.

Transitive axioms

The publication-facing declarations use only propext, Classical.choice, and Quot.sound. The project contains no axiom declarations or admitted proofs.

Finite falsifier

An independent program checked 20,272,272 bounded arbitrary tile words without finding a counterexample to the correspondence theorem. The proof does not use this computation.

Priority#

Neary’s 2013 technical report claimed M₃(5) [Neary 2013]; its refereed successor proved M₃(6) and left the four-pair case open [Neary 2015], and later literature retains M₃(6) [Bell–Potapov–Semukhin 2021] [Dong 2023]. No formal withdrawal is known. The numerical statement M₃(5) is therefore not new. No accepted proof of it, or of binary GPCP(4), was found; the proof here is the fixed-boundary theorem for Neary’s four 2015 pairs followed by prior endpoint absorption. The repository’s novelty audit records the search.

Complete source repositoryManuscript, Lean development, verification suite, falsifier, references, and version history

References#

Turlough Neary, Undecidability in Binary Tag Systems and the Post Correspondence Problem for Four Pairs of Words, arXiv:1312.6700v1, 2013. The earlier M₃(5) claim, not retained in the refereed successor.
Turlough Neary, Undecidability in Binary Tag Systems and the Post Correspondence Problem for Five Pairs of Words, STACS 2015. The binary tag systems and the four simulation pairs.
Julien Cassaigne, Vesa Halava, Tero Harju, and François Nicolas, Tighter Undecidability Bounds for Matrix Mortality, Zero-in-the-Corner Problems, and More, 2014. The previous antichain, word-pair matrices, and generator packing.
François Nicolas, (Generalized) Post Correspondence Problem and Semi-Thue Systems, 2008. GPCP conventions and prior open cases.
Vesa Halava, Tero Harju, and Mika Hirvensalo, Undecidability Bounds for Integer Matrices Using Claus Instances, 2007. Rank-one endpoint absorption.
Günter Rote, Probabilistic Finite Automaton Emptiness Is Undecidable for a Fixed Automaton, MFCS 2025. Diagnosis of the terminal-pair error and a replacement.
Paul C. Bell, Igor Potapov, and Pavel Semukhin, On the Mortality Problem, 2021. Later mortality bounds.
Ruiwen Dong, Recent Advances in Algorithmic Problems for Semigroups, 2023. Survey.