MATRIX SEMIGROUPS · WORKING NOTE · 21 JULY 2026

Five 3 × 3 integer matrices suffice for undecidable mortality

The conventional reduction needs five matrices to encode a Post correspondence instance and a sixth to annihilate a detected match. A forced terminal tile can do both jobs.

ETERNALISTALGEBRAIC CORE VERIFIED IN LEAN 4

Abstract

Mortality asks whether the zero matrix belongs to the multiplicative semigroup generated by a finite family of matrices. We show that this problem is undecidable for families of at most five 3 × 3 integer matrices. Four generators are nonsingular and upper triangular; the fifth is nonzero of rank one. The reduction absorbs the forced last pair in the corrected Neary–Rote five-pair PCP construction into the rank-one annihilator that ordinarily costs an additional generator.

Theorem. M₃(5) is undecidable, even when four generators are nonsingular upper-triangular integer matrices and the fifth is a nonzero integer matrix of rational rank one.

READ THE FIVE-PAGE NOTE · PDF FORMALIZATION ENVELOPE

1. Mortality and the missing generator

For a finite family 𝒜 of square matrices, the mortality problem asks whether some nonempty product of members of 𝒜 is the zero matrix. Write M_d(k) for the problem restricted to at most k rational d × d generators. Integer inputs have the same decidability status.

A k-pair instance of the Post correspondence problem gives k nonsingular 3 × 3 matrices whose (1,3) entry vanishes exactly when the two accumulated words match. The usual construction then introduces a rank-one separator to turn that single zero entry into the zero matrix. Five PCP pairs therefore appear to demand six matrix generators.

The corrected five-pair source has more structure: pair 5 is forced to occur exactly once, at the end of every primitive solution. Multiplying its encoding into the separator fuses the terminal symbol and the annihilator.

2. The ternary matrix morphism

Recode the binary alphabet as the nonzero ternary digits 1 and 2. For a word x, let σ(x) be its base-3 value and |x| its length. Define

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

This is a morphism: Ψ(xx′, yy′) = Ψ(x, y)Ψ(x′, y′). Positional notation with nonzero digits is injective, so the distinguished entry Ψ(x, y)_1,3 vanishes exactly when x = y. Its determinant is 3^|x|+|y|, hence every encoded pair is nonsingular.

3. Terminal absorption

Let X_i = Ψ(u_i, v_i) encode the five PCP pairs. Keep the first four matrices and replace the fifth by

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

Because X₅ is nonsingular, c = X₅e₃ is nonzero and A₅ has rank one. If w is a terminal PCP match, then

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

The converse is the important part

A zero product cannot avoid A₅, because the other four matrices are nonsingular. Split an arbitrary product at every occurrence of A₅:

Y = P_{0} A_{5} P_{1} A_{5} \dots A_{5} P_{t} .

Each P_j is a possibly empty product of X₁, …, X₄. Expanding A₅ = ce₁^T factors Y into two nonzero boundary vectors and the internal scalars e₁^TP_jc. Therefore Y can vanish only if one internal scalar vanishes. That scalar is exactly the (1,3) entry of X_wX₅, so it exposes a terminal PCP match. This covers arbitrary products, adjacent copies of A₅, and empty internal blocks.

4. Consequences

Combining terminal absorption with the Neary–Rote terminal five-pair source proves M₃(5) undecidable. Standard dimension–generator trades sharpen the bounded-mortality frontier to

M₃(5) · M₅(4) · M₆(3) · M₁₂(2).

Padding with a zero direct summand propagates the five-generator result to every dimension d ≥ 3. The same trade resolves the previously open three-generator cells in dimensions 6, 7, and 8, and the two-generator cells in dimensions 12, 13, and 14.

5. What the machine checked

The accompanying Lean 4 development is pinned to mathlib 4.12.0. It proves the exact integer terminal-absorption equivalence for arbitrary nonempty generator words, the primitive-solution descent needed to pass from ordinary PCP solvability to terminal matching, preservation and reflection of zero under ℤ ↪ ℚ, and the exact rank-one claim for the exceptional generator. It contains no admitted statements or project axioms.

The internal correctness of the published tag-system-to-five-pair-PCP simulation remains an external theorem. The formal artifact verifies the entire new algebraic reduction conditional on that source result; it does not re-formalize Neary and Rote’s tag-system construction.

Status and novelty. The numerical statement M₃(5) appeared in a 2013 preprint through a four-pair PCP claim that was subsequently abandoned. The accepted 2015 result yields six matrices. The terminal rank-one absorption presented here appears to supply the first valid five-matrix route, but that novelty assessment remains subject to specialist and author confirmation.

References

P. C. Bell, I. Potapov, and P. Semukhin, On the mortality problem, Information and Computation 281 (2021).
J. Cassaigne, V. Halava, T. Harju, and F. Nicolas, Tighter undecidability bounds for matrix mortality (2014).
V. Halava, T. Harju, and M. Hirvensalo, Undecidability bounds for integer matrices using Claus instances (2007).
T. Neary, Undecidability in binary tag systems and the Post correspondence problem for five pairs of words (2015).
G. Rote, Probabilistic finite automaton emptiness is undecidable for a fixed automaton (2025).