M₄(4): Mortality of Four 4 × 4 Integer Matrices

Matrix mortality for four 4 × 4 integer matrices is undecidable: M₄(4).

Three of the matrices are the controls of the paired scalar series, which share first column e₁ and include a permutation matrix; the fourth is a rank-one separator. Two of the controls are singular, so the standard converse for rank-one separators does not apply; the common fixed column replaces it. The previous four-generator bound was M₅(4).

The three controls alone prove scalar zero reachability Z̊₄(3) undecidable, and hence Z₄(3) and R₅(3).

Known Stuff#

Bounds before this work#

After M₃(5), the minimal known undecidable mortality cells were

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

The four-generator cell M₅(4) is due to Cassaigne, Halava, Harju, and Nicolas [Cassaigne et al. 2014]. This article lowers its dimension to four.

The paired scalar series#

The paired scalar series replaces the four tiles of fixed-boundary correspondence by two data controls G_b, G_c and a toggle T, all integer 4 × 4 matrices. With the column c = (μ, −1, t, 0)^T, where μ = σ(M) and t = 3^|M|, a nonempty control word z with

e_{1}^{T} G_{z} c = 0

exists exactly when the tag system halts. The explicit matrices have two properties used below: all three fix e₁, and the data controls are singular. Toggle-only words have coefficient μ ≠ 0.

Scalar and corner problems#

Scalar zero reachability Z_d(k) supplies a row L, a column C, and at most k integer d × d matrices, and asks whether LYC = 0 for some nonempty product Y. The structured problem Z̊_d(k) additionally requires every generator to have first column e₁. The corner problem R_d(k) fixes L and C to coordinate vectors, and Z_d(k) ≤_m R_d+1(k) [Cassaigne et al. 2014].

New Stuff#

Result#

M₃(5) spends four generators on the tiles and one on the separator. The paired series does the work of the four tiles with three matrices in dimension four, so adding the separator ce₁^T gives four generators. The standard converse for a rank-one separator uses nonsingular ordinary generators to show that the outer factors of a product never vanish, and here the data controls are singular. The common fixed column e₁ does the same job: it keeps every row e₁^TQ nonzero, and a column Qc can vanish only if its own coefficient does.

Theorem (M₄(4)). A primitive-recursive map sends every program to four 4 × 4 integer matrices, three with first column e₁, one of them a permutation matrix, and one nonzero of rank one, that are mortal exactly when the program halts. Hence M₄(4) is undecidable.

Theorem (Z̊₄(3)). Scalar zero reachability for three 4 × 4 integer matrices with common first column e₁ is undecidable.

From a scalar zero to mortality#

Adjoin the outer product

S = c e_{1}^{T} = [\begin{matrix} μ & 0 & 0 & 0 \\ - 1 & 0 & 0 & 0 \\ t & 0 & 0 & 0 \\ 0 & 0 & 0 & 0 \end{matrix}]

to G_b, G_c, T. It is a nonzero integer matrix of rank one.

Forward implication#

If a control product Q satisfies e₁^TQc = 0, then

S Q S = c (e_{1}^{T} Q c) e_{1}^{T} = 0 .

Arbitrary products#

A product without S fixes e₁ and is therefore nonzero. A product with r ≥ 1 copies of S has a unique form

Q_{0} S Q_{1} S \dots S Q_{r} = (Q_{0} c) [\prod_{1 \leq i < r} e_{1}^{T} Q_{i} c] (e_{1}^{T} Q_{r}),

where each Q_i is a possibly empty control product. The final row is nonzero because Q_re₁ = e₁ gives (e₁^TQ_r)e₁ = 1. If the product is zero, then either Q₀c = 0, in which case Q₀ is nonempty because c ≠ 0 and e₁^TQ₀c = 0, or some inner scalar e₁^TQ_ic vanishes, in which case Q_i is nonempty because an empty block contributes μ ≠ 0. Either way some nonempty control word has zero paired coefficient, and the tag system halts.

Consequences#

The instance (e₁^T, c; G_b, G_c, T) of Z̊₄(3) has a zero exactly when the tag system halts, which proves the second theorem. Dropping the structural condition gives Z₄(3), and the reduction to corners gives R₅(3). The decidability table records the current mortality frontier.

Bookkeeping#

Verification and provenance#

Paired compression

Lean checks the separated coordinates, the agreement plane, the explicit matrices, the coefficient identity for every control word, and decoder surjectivity.

Mortality equivalence

Lean checks every number and placement of separators, the common-column converse with singular data controls, integrality, and that the separator is nonzero of rank one over ℚ.

Transitive axioms

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

Independent falsifier

A separate exact-arithmetic program checks bounded arbitrary role words, compressed coefficients, decoder coverage, and arbitrary products of the four matrices. The proof does not use it.

Formal scope#

The equivalence from the tag semantics to mortality of the four integer matrices is machine-checked as nearyMortality44_mortal_iff_tagHaltsFrom. The computable reduction from mathlib’s code-halting predicate, through a fixed universal machine, a two-tag system, a cyclic tag system, and Neary’s compiler, is also machine-checked: Lean proves the four-matrix constructor primitive recursive, codeHalts_reduces_mortality44, and mortality44_not_computable, and assumes no external universality theorem. The priority claim is outside Lean.

Priority#

Searches of public literature through 22 July 2026 found no prior proof of M₄(4) or of Z̊₄(3). The closest earlier bounds are M₅(4) and the structured Z₅(3) [Cassaigne et al. 2014]. The anti-diagonal quotient is standard linear algebra and the rank-one separator is prior art; no source was found for the paired-role decoder, the four-dimensional scalar theorem, or the common-column converse.

References#

GPT-5.6 Sol, elicited by @eternalism_4eva, M₃(5): Mortality of Five 3 × 3 Integer Matrices, 2026. Fixed-boundary correspondence and the rank-one separator.
GPT-5.6 Sol, elicited by @eternalism_4eva, The Paired Scalar Series, 2026. The three controls and their decoder.
Turlough Neary, Undecidability in Binary Tag Systems and the Post Correspondence Problem for Five Pairs of Words, STACS 2015. The binary tag systems.
Julien Cassaigne, Vesa Halava, Tero Harju, and François Nicolas, Tighter Undecidability Bounds for Matrix Mortality, Zero-in-the-Corner Problems, and More, 2014. Definitions, prior bounds, and the scalar-to-corner reduction.