M₈(2): Mortality of Two 8 × 8 Integer Matrices

Matrix mortality for two 8 × 8 integer matrices is undecidable: M₈(2).

Two constructions present the paired scalar series with two matrices, a transition A and a cut UO, whose returns OAⁿU are the toggle and the two data controls at times 0, 1, 2 and multiples of one rank-one separator afterwards. The dimension such a pair needs is a Hankel rank that depends on the separator’s row. A row that keeps exactly the zeros of the paired series gives dimension nine and proves M₉(2); at a benchmark source, every row of that kind needs at least nine dimensions. Dimension eight forces a row that accepts zeros in only one of the two phases; prepending a toggle to a control word recovers every rejected zero, so the existence of a zero, and hence halting, is preserved.

Both reductions are primitive recursive and produce integer matrices. Zero padding gives M_d(2) for every d ≥ 8. The previous bounds were M₁₀(2) in this series and M₁₅(2) in the literature. M₇(2) remains open.

Known Stuff#

Two-generator mortality#

M_d(2) asks whether some nonempty product of two given d × d integer matrices is zero; a single matrix counts as a pair with a repeated generator. Every word in the two matrices counts, with no grammar. Before this series the best bound was M₁₅(2) [Cassaigne et al. 2014]. Generator packing applied to M₃(5) gives M₁₂(2), and the binary prefix decoder gives M₁₀(2).

The paired source#

The paired scalar series has integer 4 × 4 controls G_b, G_c, T and boundary column c. For a Neary tag system with width β ≥ 3 and body B, put

\begin{array}{l} ρ = 3^{β}, μ = σ (M) = \frac{5 ρ - 1}{2}, t = 3^{| M |} = 3 ρ, \\ W = H (B), K = 3^{| W | + 3}, V = σ (1 W 10) . \end{array}

Here M = 10^β is the boundary word, H the letter code, and 1W10 the lower word of the tile R_c, so K and V are its length power and ternary value. The constructions below use the column after one toggle,

u = T c = {(μ, 0, t, - 1)}^{T} .

For a control word z, G_zu = G_zTc is one of the two phase columns: with X the decoded upper word followed by M, Y the decoded lower word, and h = σ(X) − σ(Y),

G_{z} u = {\begin{cases} {(h, - 3^{| Y |}, 3^{| X |}, 0)}^{T} & rule phase, \\ {(h, 0, 3^{| X |}, - 3^{| Y |})}^{T} & deletion phase. \end{cases}

The lower word Y is a concatenation of the tiles’ lower words 0, 110, and 1W10; no legality of the decoded computation is assumed. Some nonempty control word has h = 0 exactly when the tag system halts. Prepending T to z switches the phase and keeps X and Y.

Returns of one transition and one cut#

Take a transition A, maps U from ℚ⁴ into its space and O back, and the cut C = UO. The returns are Γ_n = OAⁿU. By singular-return compression, if no power of A vanishes, then {A, C} is mortal exactly when {Γ_n : n ≥ 0} is. If moreover every return is a nonzero multiple of one of finitely many matrices and each of them occurs, the returns may be replaced by those matrices (finitely many return shapes).

Both constructions aim at the four shapes T, G_b, G_c, and a rank-one separator ur for a row r with first entry 1. Every control fixes e₁, so rG_z is never zero, and G_zu = 0 already implies rG_zu = 0. The argument of M₄(4) then shows that, when ru ≠ 0,

Mortal {T, G_{b}, G_{c}, u r} \Leftrightarrow \exists z \neq ε : r G_{z} u = 0 .

The whole design problem is therefore to choose r so that the right side is equivalent to halting, and to realize the four shapes as returns in as few dimensions as possible.

Realizing a return sequence#

Finding (A, U, O) with prescribed matrices OAⁿU is the classical realization problem of linear systems theory: the least possible dimension is the rank of the block Hankel matrix [Γ_i+j]_i,j≥0 [Ho–Kalman 1966]. The lower bound is immediate, since Γ_i+j = (OAⁱ)(A^jU) factors through the state space.

The sequences here are geometric after time two: Γ_n = ξ²⁻ⁿS for n ≥ 3, with ξ ≠ 0 and S of rank one. Extrapolate the tail backward and subtract it:

N_{n} = Γ_{n} - ξ^{2 - n} S (n = 0, 1, 2), N_{n} = 0 (n \geq 3) .

Splitting A into its nilpotent and invertible parts splits any realization into one of the extrapolated tail, which needs at least rank S = 1 dimension, and one of the residuals N₀, N₁, N₂. The nilpotent part is a sum of Jordan chains, and a chain of length ℓ contributes only at times 0, …, ℓ−1. The minimal numbers of chains are

c₃ = rank N₂ chains of length three;
c₂ chains of length two, the rank of N₁ as a map from ker N₂ to ℚ⁴/im N₂, which is the part of N₁ that the longer chains cannot supply;
c₁ chains of length one, for what remains of N₀.

The least dimension is 3c₃ + 2c₂ + c₁ + 1, the Hankel rank of the sequence.

New Stuff#

Result#

Aim the returns at G_c at time two, G_b at time one, a multiple of T at time zero, and multiples of ur afterwards. The data control G_c has rank three, with kernel spanned by

κ = {(K - 3 V, 3, 0, - K)}^{T} .

Subtracting a rank-one tail term ur can lower its rank to two only if rκ = 0. Each chain count therefore turns into a linear condition on the row r:

Separator row	`c`₃	`c`₂	`c`₁	Dimension	Zeros kept
`e`₁^T, the paired row	3			at least 10	all
(1, `q`, `q`, `q`) with `rκ` = 0	2	1	0	9	all
(1, `a`, `q`, `q`) with `rκ` = `rη` = 0	2	0	1	8	deletion phase only

The paired row fails because e₁^Tκ = K − 3V ≠ 0. A row keeps every zero of the paired series only if it vanishes on both phase columns of every solution, where h = 0 and |X| = |Y|; that forces its last three entries to be equal. Such a uniform row can satisfy rκ = 0, which fixes its slope and gives dimension nine. Removing the chain of length two needs the second condition rη = 0, where G_cη = G_bκ, and no nonzero uniform row satisfies both conditions. A row satisfying both exists once the rule-phase entry is allowed to differ. It rejects the rule-phase members of solutions, and prepending a toggle turns every such solution into an accepted deletion-phase one.

The table explains the two designs; the proofs below construct the realizations directly and do not depend on the count.

Theorem (M₈(2)). A primitive-recursive map sends every program to two 8 × 8 integer matrices that are mortal exactly when the program halts. Hence M_d(2) is undecidable for every d ≥ 8.

Theorem (M₉(2)). A primitive-recursive map sends every program to two 9 × 9 integer matrices that are mortal exactly when the program halts. The separator of this construction vanishes on exactly the control words at which the paired series, after one appended toggle, vanishes.

Dimension nine: keeping every zero#

A uniform row (1, s, s, s) reads both phase columns the same way:

(1, s, s, s) G_{z} u = F_{s} (X) - F_{s} (Y), F_{s} (x) = σ (x) + s 3^{| x |} .

Tilted codes#

The tilted code F_s is injective on binary words whenever s < −3/2. A word of length n has (3ⁿ − 1)/2 ≤ σ(x) ≤ 3ⁿ − 1, so F_s maps the words of each length into an interval, and for s < −3/2 these intervals are disjoint and move down as n grows. Within one length, F_s differs from the injective σ by a constant. Hence (1, s, s, s)G_zu = 0 exactly when X = Y, which is exactly when the paired coefficient of zT vanishes. The row keeps every zero, only shifted by one appended toggle.

The slope required by rκ = 0 is

q_{9} = \frac{K - 3 V}{K - 3},

and the syntax of the tag source gives q₉ < −3/2 for every body. The tilted separator is u(1, q₉, q₉, q₉).

The nine-dimensional realization#

The target sequence is

Γ_{n} = {\begin{cases} T, & n = 0, \\ G_{b}, & n = 1, \\ G_{c}, & n = 2, \\ ν^{n - 3} S_{9}, & n \geq 3, \end{cases}

with ν ≠ 0 and S₉ a nonzero multiple of the tilted separator. Because rκ = 0, a suitably normalized tail makes rank N₂ = 2, which gives two chains of length three. The row is uniform, so rη ≠ 0 and one chain of length two remains; the tail is tuned so that no chain of length one is needed. With the eigenline of the tail this gives

A \sim J_{3} (0) \oplus J_{3} (0) \oplus J_{2} (0) \oplus [ν], 3 + 3 + 2 + 1 = 9 .

An exact symbolic program constructs this factorization, and Lean checks the resulting rational 9 × 9 transition, 9 × 4 input, and 4 × 9 output and every return. The denominators and pivots are nonzero whenever β > 0 and B contains b, which holds for every body produced by the universal source.

The floor for uniform rows#

Fix the benchmark source β = 3, B = bb. Consider every return sequence equal to T, G_b, G_c at times 0, 1, 2 and to any rational multiple of νⁿ⁻³u(1, q, q, q) afterwards, for any rational ν and any rational q < −3/2. Every exact realization of such a sequence has dimension at least nine. Zero-preserving uniform rows therefore cannot give dimension eight with this design, even after retuning the tail. The bound concerns this family of exact realizations; it says nothing about M₈(2) itself.

Dimension eight: keeping some zero#

A row r = (1, a, q, q) reads the two phase columns differently:

r G_{z} u = {\begin{cases} F_{q} (X) - F_{a} (Y) & in rule phase, \\ F_{q} (X) - F_{q} (Y) & in deletion phase. \end{cases}

With

η = {(K - 3 V + 48, 0, 0, 27 - K)}^{T},

the two conditions rκ = rη = 0 determine both slopes:

q = \frac{K - 3 V + 48}{K - 27} = - 1 - θ, a = 16 + 9 q = 7 - 9 θ, θ = \frac{σ (W)}{3^{| W |} - 1} .

Here θ is the periodic ternary value of W. Since W begins with 1 and contains 0, 1/2 < θ < 1, so −2 < q < −3/2 and a > −2. By the tilted-code injectivity, the deletion-phase value vanishes exactly when X = Y. The rule-phase value compares two different codes, and its possible zeros are the new obligation.

The wrong-phase exclusion#

The rule-phase value F_q(X) − F_a(Y) never vanishes, for any upper word X and any lower word Y built from the lower tiles. The proof uses one more property of the universal source: every body it emits begins with bcb, so

W = H (b) H (c) H (b) \dots = 1 0^{β} 1 1 1 0^{β} 1 \dots .

Suppose F_q(X) = F_a(Y).

One word is a suffix of the other

The slopes have denominator 3^|W| − 1, which is prime to 3. Multiply by it and reduce modulo 3^m, where m is the shorter length: the terms with 3^|X| and 3^|Y| disappear, so σ(X) ≡ σ(Y) modulo 3^m. The last m ternary digits agree, so the shorter word is a suffix of the longer.

The lower word is longer

If |X| = |Y|, then X = Y and q = a = 16 + 9q, so q = −2, which is excluded. If X = pY with p nonempty, cancelling Y gives F_q(p) = a; but F_q(p) ≤ 3^|p|(1 + q) − 1 < −2 < a. So Y = pX with p nonempty.

A period equation

With k = |p|, cancelling X gives q = σ(p) + a3^k, and substituting q = −1 − θ, a = 7 − 9θ,

θ = \frac{σ (10 p) + 1}{3^{k + 2} - 1} .

Clearing denominators and reducing modulo 3, the fact that W ends in 1 forces p to end in 0. Let p⁺ be p with that final 0 changed to 1 and put P = 10p⁺, so that σ(P) = σ(10p) + 1. Then θ is the periodic value of both W and P, and cross-multiplying shows σ(WP) = σ(PW). By injectivity of σ,

W P = P W .

Commuting words are powers of a common word, so P is a prefix of the infinite repetition W^ω and P^ω = W^ω. In particular p⁺ consists of the letters of W^ω in positions 2, …, k+1, counting from 0.

No length survives

After its first two letters, W reads 0^β−11110^β1⋯. A lower word is a concatenation of 0, 110, and 1W10, so its first 1 is followed by 10. The prefix p of Y agrees with p⁺ except in its last letter.

k ≤ β − 1: then p⁺ = 0^k, which does not end in 1.
k = β: then P = H(b), whose repetition continues 10, while W continues 11.
k = β + 1: then p = 0^β−110, whose first 1 is followed by 0, so p is not a prefix of a lower word.
k = β + 2: then P = H(bcc). Its repetition has 1 in position β+4, where W has the first 0 of its second H(b).
k ≥ β + 3: then p begins 0^β−1111, again not a prefix of a lower word.

Cases 3 and 5 use the lower-word grammar and cases 2 and 4 the period; neither argument alone suffices.

Recovering every witness#

The row r therefore vanishes exactly on the deletion-phase columns with X = Y. Each such zero is a zero of the paired series. Conversely, if z is a nonempty control word with X = Y in rule phase, then Tz has the same X and Y in deletion phase. The empty word gives ru ≠ 0, because its upper word is M and its lower word is empty. Hence

\exists z \neq ε : r G_{z} u = 0 \Leftrightarrow the tag system halts.

This is existential zero transport: the set of zero words changes, but whether it is empty does not.

The eight-dimensional realization#

Define

\begin{array}{l} λ = 2 q + 1, h = \frac{6}{λ (3 ρ - 1)}, ξ = 3 ρ + 1 + ρ h, S = h u r, \\ Δ = K ((λ - 2) ρ - λ) + 26 λ + 72, γ = \frac{K (λ (27 ρ^{3} - 1) + 18 ρ^{2} + 6 ρ)}{Δ} . \end{array}

Here λ < −2, ρ ≥ 27, and K > 27, so |ρh| < 2 and ξ > 0. Moreover

\begin{array}{l} Δ < K (2 - 4 ρ) + 20 < 0, \\ λ (27 ρ^{3} - 1) + 18 ρ^{2} + 6 ρ < - 54 ρ^{3} + 18 ρ^{2} + 6 ρ + 2 < 0, \end{array}

so γ > 0 and h ≠ 0; no scaling or denominator vanishes. The target sequence is

Γ_{n} = {\begin{cases} γ T, & n = 0, \\ G_{b}, & n = 1, \\ G_{c}, & n = 2, \\ ξ^{2 - n} S, & n \geq 3, \end{cases}

with residuals

N_{0} = γ T - ξ^{2} S, N_{1} = G_{b} - ξ S, N_{2} = G_{c} - S .

The normalization of h makes rank N₂ = 2, with kernel spanned by κ and

z = {(\frac{3 ρ - 1}{6}, 0, ρ, - \frac{1}{3})}^{T}, G_{c} z = u;

the choice of ξ makes N₁ map that kernel into the image of N₂. The residuals therefore need two chains of length three and one of length one, and the tail needs one eigenline: 3 + 3 + 1 + 1 = 8.

The factorization#

The chains can be written down without choosing a basis by a rank test. Let E be the 4 × 2 matrix with columns e₁ and e₃, put L_i = N_iE, and let

Λ = [\begin{matrix} 0 & 0 & - q / 3 & (3 ρ - λ) / 6 \\ 0 & 0 & 1 / 3 & ρ \end{matrix}], Q_{2} = [\begin{matrix} 1 & a + K (3 ρ - λ) / 6 & 0 & (3 ρ - 1) / 2 \\ 0 & ρ K & 1 & 3 ρ \end{matrix}] .

Then ΛL₂ = I₂, and N₂ = L₂Q₂ is a rank factorization through the first and third coordinates. The other factors correct the residuals one time step at a time:

\begin{array}{l} Q_{1} = Λ (N_{1} - L_{1} Q_{2}), N_{0}^{'} = N_{0} - L_{0} Q_{2} - L_{1} Q_{1}, \\ f = (0, 0, 0, γ), j = - 3 N_{0}^{'} z / γ, Q_{0} = Λ (N_{0}^{'} - j f) . \end{array}

The row f is the second row of N₀, and jf is the part of the time-zero remainder outside the image of L₂: the chain of length one. Substitution gives

\begin{array}{l} N_{2} = L_{2} Q_{2}, \\ N_{1} = L_{1} Q_{2} + L_{2} Q_{1}, \\ N_{0} = L_{0} Q_{2} + L_{1} Q_{1} + L_{2} Q_{0} + j f . \end{array}

Write the state as (x₀, x₁, x₂, y, g) with x_i ∈ ℚ² and y, g ∈ ℚ. The blocks x₀, x₁, x₂ are the three levels of the two chains of length three, y is the chain of length one, and g is the eigenline:

\begin{array}{l} A (x_{0}, x_{1}, x_{2}, y, g) = (0, x_{0}, x_{1}, 0, ξ^{- 1} g), \\ U v = (Q_{2} v, Q_{1} v, Q_{0} v, f v, ξ^{2} h r v), \\ O (x_{0}, x_{1}, x_{2}, y, g) = L_{0} x_{0} + L_{1} x_{1} + L_{2} x_{2} + j y + u g . \end{array}

Each application of A moves the chain blocks one level down, kills y, and scales g by ξ⁻¹. The factor identities give Γ₀, Γ₁, Γ₂. From time three on only g survives and gives ξ²⁻ⁿS, and the eigenvalue ξ⁻¹ ≠ 0 shows that no power of A vanishes.

Two matrices#

In both realizations the transition has a nonzero eigenvalue, so no power vanishes and singular-return compression identifies mortality of {A, UO} with mortality of the returns. Every return is a nonzero multiple of T, G_b, G_c, or the separator, and times 0, 1, 2, 3 supply all four, so the returns may be replaced by these four shapes. By the separator argument, the four shapes are mortal exactly when some nonempty control word has zero separator coefficient. In dimension nine that happens exactly when the paired series has a zero; in dimension eight, by existential transport, exactly when the tag system halts.

In dimension nine the separator coefficient of z vanishes exactly when the paired coefficient of zT does. In dimension eight the two sets of zero words differ, and only their nonemptiness agrees.

Integer matrices and effectivity#

Denominator clearing#

Both realizations have rational entries. Multiply each generator by a nonzero integer d_i that clears its denominators; the two factors may differ. For every nonempty word,

{\hat{G}}_{i_{1}} \dots {\hat{G}}_{i_{n}} = (\prod_{k = 1}^{n} d_{i_{k}}) G_{i_{1}} \dots G_{i_{n}}, {\hat{G}}_{i} = d_{i} G_{i} \in ℤ^{d \times d},

so the integer product is zero exactly when the rational product is. For a computable reduction the entries must also be computed without searching. They are evaluated as unreduced numerator–denominator pairs, for which addition, multiplication, division by a nonzero value, and fixed powers are primitive recursive without any greatest-common-divisor computation; one common denominator per generator is accumulated from them. Neither construction uses a numerical rank test, a chosen pivot, or a basis search at run time.

The universal reduction#

Let CodeHalts(e) state that mathlib’s universal partial recursive code e halts on input zero; this predicate is not computable. A fixed universal two-tag system is compiled through Cook’s cyclic tag construction and Neary’s compiler into a width β > 2 and a body B_e, primitive recursive in e, that is long enough, has length divisible by β − 1, and begins with bcb. The checked tag theorem gives

CodeHalts (e) \Leftrightarrow the tag system (β, B_{e}) halts \Leftrightarrow the emitted integer pair is mortal.

The composed map is primitive recursive, so it is a many-one reduction from a noncomputable predicate, and both mortality problems are undecidable. Adjoining a zero block, G_i ↦ G_i ⊕ 0_n, is primitive recursive and preserves and reflects every zero product, which gives every larger dimension.

M₇(2) remains open. The floor for uniform rows concerns exact realizations of one family of return sequences; the eight-dimensional construction avoids it by changing both the return sequence and the set of zero words.

Bookkeeping#

Verification and provenance#

The M₈(2) proof was reviewed at commit 6f8ae3a858daf28401732cecd043ed209ec4c17c and compiles with Lean and mathlib v4.33.1. The target scripts/check.sh m82 runs source-policy scans, every default environment linter in the proof closure, exact transitive-axiom comparisons, and probes that pin the final theorem types.

M₈(2) endpoint

mortality82Reduction, the many-one theorem, noncomputability, and mortality8Plus_not_computable for every padded dimension.

Wrong-phase exclusion

The period argument (no_asymmetric_period, wrongPhase_ne) for every upper word and every lower-tile word, and the bcb prefix (source_body_take_three).

Existential transport

Deletion-phase acceptance, recovery by a leading toggle, and the nonzero empty coefficient.

Eight-dimensional realization

The factor identities factor_two, factor_one, factor_zero, uniformly in the source; every return; and the mortality assembly for unrestricted products.

Eight-dimensional integer pair

Unreduced fractions, per-generator denominators, and primitive recursiveness of every entry.

Tilted separator

tiltedTernaryCode_injective, the source bound nearyTailRatio_lt_neg_three_halves, and nearyTiltedPairedCoefficient_eq_zero_iff for every control word and both phases.

Nine-dimensional realization

The explicit rational matrices and the return modules zero_moment, moment_one, moment_two, and moment_add_three, with nonzero denominators on the whole source.

M₉(2) endpoint

mortality92Reduction, mortality92Instance_primrec, codeHalts_reduces_mortality92, mortality92_not_computable, and mortality9Plus_not_computable, with the effectivity module ChangedSeparatorEffectivity.

Floor for uniform rows

nine_le_card_of_tilted_geometric_transfer_moments, a uniform 9 × 9 Hankel minor, and benchmark_return_eq_moment, which identifies the checked construction with the benchmark family.

Transitive axioms

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

Formal scope#

For both theorems Lean checks the source compiler, the separator coefficients for every control word, every return, unrestricted physical products including transitions before the first and after the last cut, denominator clearing, primitive recursiveness, the many-one reduction, noncomputability, and padding. No proof depends on a finite search, floating-point arithmetic, or an unproved invertibility.

The chain-count table and the necessity of rκ = rη = 0 in dimension eight are recorded in the audit and are not formalized; the proofs do not use them. The statement that Λ is a left inverse of L₂ is checked by the symbolic program; Lean checks the factor identities directly. The floor for uniform rows is formalized at the benchmark source only. The symbolic programs’ bounded word enumerations are auxiliary.

Priority#

Searches of public literature through 24 July 2026 found no proof of M_d(2) for any d < 15 outside this series [Cassaigne et al. 2014]. M₉(2) was completed on 31 August 2026 and M₈(2) on 5 September 2026. Return realizations, rank-one separators, alphabet reduction, and denominator clearing are prior techniques. Priority is claimed for the two theorems and their constructions, not for those techniques. Machine checking is not external peer review.

References#

GPT-5.6 Sol, elicited by @eternalism_4eva, M₃(5): Mortality of Five 3 × 3 Integer Matrices, 2026. The tag source and fixed-boundary correspondence.
GPT-5.6 Sol, elicited by @eternalism_4eva, The Paired Scalar Series, 2026. The three controls, the decoder, and the phase columns.
GPT-5.6 Sol, elicited by @eternalism_4eva, Interface Compression, 2026. Singular-return compression and finitely many return shapes.
GPT-5.6 Sol, elicited by @eternalism_4eva, Z₆(2) and M₁₀(2): Binary Compilers, 2026. The previous bound M₁₀(2).
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. The bound M₁₅(2).
B. L. Ho and R. E. Kalman, Effective Construction of Linear State-Variable Models from Input/Output Functions, Regelungstechnik 14, 1966. Minimal realization of a matrix sequence by the rank of its block Hankel matrix.