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

Matrix mortality for two 8 × 8 integer matrices is undecidable. A primitive-recursive map sends each program to an integer pair with a nonempty zero product exactly when the program halts.

The construction replaces the preceding nine-dimensional separator by one that accepts only one of the two paired phases. A leading toggle recovers every discarded witness. This weaker, existential equivalence permits an eight-dimensional return realization. The proof covers unrestricted products, integer effectivity, and padding to every larger dimension. M₇(2) remains unresolved.

Known Stuff#

Matrix mortality#

A finite family of integer matrices is mortal if some nonempty product is the zero matrix. The problem M_d(k) fixes the dimension and permits at most k generators. Our formal encoding supplies exactly two named matrices; smaller nonempty families can repeat a generator.

There is no prescribed word grammar. A vanishing scalar coefficient is an intermediate problem, not the mortality conclusion.

The paired source#

The inherited source theorem represents restricted binary-tag halting by a four-dimensional scalar series. Its body is a word B over b and c, and its fixed deletion width is β > 2. The source satisfies the length and divisibility conditions stated there. Its binary encoding and parameters are

\begin{array}{l} H (b) = 1 0^{β} 1, H (c) = 1, W = H (B), L = | W |, \\ ρ = 3^{β}, K = 3^{L + 3}, V = σ (1 W 10) . \end{array}

Juxtaposition inside words means concatenation; a word exponent repeats a symbol or block. The ternary value σ uses digits 1 and 2, so finite words have unique codes.

Write the three paired controls as T, D_b, D_c. Their coordinate matrices fix the convention used here. The toggle T exchanges coordinates two and four and fixes the other two. Each data control leaves the vector in the erase phase. With one trailing toggle absorbed, the boundary column is

u = {(\frac{5 ρ - 1}{2}, 0, 3 ρ, - 1)}^{T} .

For a raw control word w, let P_w denote its matrix product. The paired decoder supplies words X, Y and one of the following forms for P = P_w. No computational legality is assumed.

P u = {\begin{cases} {(σ (X) - σ (Y), 0, 3^{| X |}, - 3^{| Y |})}^{T} & erase phase, \\ {(σ (X) - σ (Y), - 3^{| Y |}, 3^{| X |}, 0)}^{T} & rule phase. \end{cases}

The upper word includes the nonempty terminal marker. The lower word is a concatenation of the tiles 0, 110, and 1W10. The original row reads the first coordinate, which vanishes exactly when X = Y. Existence of such a nonempty control word is equivalent to source halting.

From returns to two matrices#

We seek a transition A on a smaller physical space and maps U into it and O back to the four-dimensional interface. The second supplied matrix is the cut C = UO. Its occurrences expose the return matrices $M_{n} = O A^{n} U$ .

Singular-return compression says that the physical pair is mortal exactly when the return family is mortal, provided no pure power of A vanishes. This reduces the construction to realizing a suitable interface sequence in eight dimensions.

New Stuff#

Result#

Eight-dimensional mortality theorem. There is a primitive-recursive map from program codes to pairs of 8 × 8 integer matrices whose mortality is equivalent to halting. Consequently M₈(2) is undecidable.

The preceding nine-dimensional construction preserved the zero coefficient of every word. That is more than a decision reduction needs. Here some witnesses disappear, but a computable word transformation replaces each of them. This distinction permits one fewer dimension without contradicting the nine-state lower bound for the previous return family.

The asymmetric separator#

The universal compiler gives more than a leading b: every emitted body begins bcb. The first three compiler tracks are constant b, c, b, and the final-letter deletion removes none of them. This is proved uniformly in source_body_take_three.

The changed row must fit the residual factorization below. Write it as $r = (1, a, q, q)$ . We impose that it annihilate the two columns

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

Solving these two linear equations fixes both slopes:

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

Because W begins with 1 and contains 0, its periodic ternary value satisfies $\frac{1}{2} < θ < 1$ . Hence $- 2 < q < - \frac{3}{2}$ . For the tilted code

F_{s} (X) = σ (X) + s 3^{| X |},

the erase-phase coefficient is $F_{q} (X) - F_{q} (Y)$ . Injectivity makes its zeros exactly the word equalities. The rule-phase coefficient instead compares slopes q and a. Its possible new zeros are the main soundness obligation.

The wrong-phase exclusion#

Suppose $F_{q} (X) = F_{a} (Y)$ . The common denominator $3^{L} - 1$ is coprime to three. Clear it and reduce modulo the power of three determined by the shorter word. The length-scale terms disappear; cancellation of the denominator leaves equal terminal code digits. Thus the shorter word is a suffix of the longer.

Equal lengths give X = Y and q = a, which would force q = −2. If X = pY with nonempty p, suffix cancellation gives $F_{q} (p) = a$ . But the left side is below −2, while a > −2. Therefore only Y = pX, with nonempty p, remains. Writing k = |p|, cancellation gives

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

The body encoding ends in 1. Reducing the last equation modulo three after clearing denominators forces p to end in 0. Replace that last symbol by 1, obtaining p⁺, and set Z = 10p⁺. Its code is the numerator above. Equality of the two periodic fractions is exactly the finite commutation identity

W Z = Z W .

Indeed, cross multiplication is equality of the codes of these two concatenations. Finite-word injectivity proves the identity without an appeal to infinite radix expansions.

The prefix bcb now excludes every possible length of p. Every nonzero lower tile begins 110, so the first 1 in a lower word must be followed by 10.

If k ≤ β − 1, commutation puts the final symbol of p⁺ inside the initial zero run of W, contradicting that it is 1.
If k = β, the proposed period is H(b). The source continues 11 after this block, whereas the period restarts with 10.
If k = β + 1, the lower word begins $0^{β - 1} 10$ , contradicting its first nonzero tile.
If k = β + 2, the proposed period is H(bcc). Its next repetition starts with 1, but the source's next symbol is the first zero in its third letter b.
If k ≥ β + 3, the lower word begins $0^{β - 1} 111$ , again contradicting its first nonzero tile.

Thus the rule-phase coefficient never vanishes. The argument covers all lower-tile words and all upper words, a stronger statement than is required on decoded computations.

Recovering every witness#

The changed row accepts precisely the erase-phase word equalities. An original rule-phase witness becomes an erase-phase witness after prepending T: this swaps phase without changing the first coordinate or the decoded words. Conversely, every changed-row zero is already an original zero.

Absorbing a trailing toggle also preserves existence: append one toggle to move between the two boundary conventions, and use $T^{2} = I$ for the reverse direction. The empty coefficient is nonzero because its upper word is the marker and its lower word is empty. Consequently

\exists w \neq ε : r P_{w} u = 0 \Leftrightarrow the restricted-tag source halts.

This is existential zero transport, not pointwise zero-language equivalence.

The eight-dimensional realization#

Keep the two data roles, rescale the toggle, and use the asymmetric rank-one separator. Define

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

Here t < −2, ρ ≥ 27, and K > 27. Consequently ρh > −2 and ξ > 0. The denominator and the bracket in the numerator of γ satisfy

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

Thus γ > 0; also h ≠ 0. No role scaling or denominator vanishes. The desired returns are

O A^{n} U = {\begin{cases} γ T & n = 0, \\ D_{b} & n = 1, \\ D_{c} & n = 2, \\ ξ^{2 - n} R & n \geq 3 . \end{cases}

Subtract the geometric tail extrapolated to times zero, one, and two:

F_{0} = γ T - ξ^{2} R, F_{1} = D_{b} - ξ R, F_{2} = D_{c} - R .

These residuals fit two length-three nilpotent chains and one static coordinate. One further coordinate carries the geometric tail. The dimension count is therefore 3 + 3 + 1 + 1 = 8. The next section supplies the factors rather than selecting a basis by a rank test.

A fixed residual factorization#

Index the four interface coordinates from zero. Let E have columns e₀ and e₂, and put $L_{i} = F_{i} E$ . Define

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

The remaining factors are successive residual corrections:

\begin{array}{l} Q_{1} = G (F_{1} - L_{1} Q_{2}), \\ Z_{0} = F_{0} - L_{0} Q_{2} - L_{1} Q_{1}, \\ z = {((3 ρ - 1) / 6, 0, ρ, - 1 / 3)}^{T}, f = (0, 0, 0, γ), \\ j = - 3 Z_{0} z / γ, Q_{0} = G (Z_{0} - j f) . \end{array}

Substitution gives the three identities checked uniformly by factor_two, factor_one, and factor_zero:

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

Use physical coordinates of sizes 2, 2, 2, 1, 1. On a vector with those five components, set

\begin{array}{l} A (x_{0}, x_{1}, x_{2}, s, 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}, s, g) = L_{0} x_{0} + L_{1} x_{1} + L_{2} x_{2} + j s + u g . \end{array}

The factor identities give the first three returns. After three steps, both nilpotent chains and the static coordinate vanish, leaving exactly the required geometric tail. Its nonzero eigenvalue also proves that no power of A is zero.

Unrestricted physical products#

Take the two physical matrices A and C = UO. A zero word containing a cut may have arbitrary initial and final transition runs. Multiplication by O on the left and U on the right retains those runs as returns:

A^{p_{0}} C \dots C A^{p_{r}} = 0 \Rightarrow M_{p_{0}} \dots M_{p_{r}} = 0 .

Conversely, a zero return product gives an actual physical word by adding exterior cuts:

C A^{p_{0}} C \dots A^{p_{r}} C = U (M_{p_{0}} \dots M_{p_{r}}) O = 0 .

Cut-free words are nonzero by the eigenline. Every return is a nonzero multiple of one of T, D_b, D_c, ur, and times 0, 1, 2, 3 supply all four roles. Relabelling and discarding these nonzero scalars preserve mortality in both directions.

The rank-one separator theorem makes mortality of this four-role family equivalent to existence of an interior coefficient rPu = 0. The empty coefficient cannot vanish. The preceding existential transport then identifies mortality of the physical pair with source halting.

Integer effectivity and padding#

The chart uses only fixed-size arrays, word codes, length powers, and rational arithmetic. Its formulas are evaluated in certified unreduced fractions whose numerators and denominators are primitive recursive. Each physical generator is multiplied by one nonzero common denominator. Every product is therefore multiplied by a nonzero scalar, preserving and reflecting zero.

The same operation-only definitions supply the rational chart and its effective interpreter. No numerical rank test, chosen pivot, or search for a basis is hidden in the reduction. Composing the primitive-recursive integer family with the universal source gives mortality82Reduction.

Adjoining a zero block is itself primitive recursive and preserves nonempty mortality. The composed theorem mortality8Plus_not_computable proves M_8+n(2) undecidable for every n ≥ 0.

Bookkeeping#

Verification#

The reviewed artifact is commit 6f8ae3a858daf28401732cecd043ed209ec4c17c. The complete endpoint and padding corollaries compile with Lean and mathlib v4.33.1. The named target runs source-policy scans, every default environment linter in its proof closure, exact transitive-axiom comparisons, and probes pinning the final theorem types:

scripts/check.sh m82

Universal endpoint: the primitive-recursive reduction, many-one theorem, noncomputability, and padding.
Wrong-phase exclusion and existential zero transport.
Fixed chart and uniform factorizations, all return moments, and unrestricted mortality assembly.
Primitive-recursive integer construction and reviewed axiom manifest.
Mathematical audit and separate exact symbolic cross-check.

The final declarations depend only on propext, Classical.choice, and Quot.sound. The symbolic program checks the uniform chart independently of Lean's expression evaluation; its bounded word enumeration is auxiliary and is not a premise of the universal proof.

Scope and provenance#

This is the standard nonempty-product problem for two integer matrices. The source compiler, wrong-phase converse, all return times, arbitrary exterior transition runs, effectivity, and dimension padding are formalized. The pointwise zero languages are deliberately different.

The construction improves this series' preceding bound from nine dimensions to eight. Its source theorem and historical literature are documented in the five-matrix source article; the intervening pointwise-preserving construction is documented in the nine-dimensional article. The present result is dated 5 September 2026. Machine checking is not external peer review, and no priority conclusion follows from the Lean theorem alone.

M₇(2) remains unresolved. The earlier exact-realization obstructions retain their stated scope; this construction escapes them by changing both the return sequence and which individual words witness a zero.