M₉(2): Two 9 × 9 Matrices via Singular Return Compression

Known Stuff#

Problem convention#

For positive integers d and k, M_d(k) is mortality for a family of at most k integer d × d matrices. The formal encoding uses k named matrices; a smaller nonempty family gives an equivalent tuple by repeating one generator. Products are read from left to right, and the empty product is excluded.

M_{d} (k) (G) \Leftrightarrow \exists n \geq 1, \exists i_{1}, \dots, i_{n} \in {0, \dots, k - 1} : G_{i_{1}} \dots G_{i_{n}} = 0_{d \times d} .

The reduction must work uniformly over all input programs and produce integer matrices. Neither a prescribed grammar of products nor a single vanishing matrix entry would settle this problem.

Paired scalar zero language#

The paired scalar interface represents a restricted tag system by three 4 × 4 controls. Here they are named T, D_b, D_c: a toggle and two data controls. These data controls are the G_b, G_c of the paired article, not the original deletion tiles. Let β be the deletion width and B the body in the rule $c \mapsto B b$ . Under the source hypotheses $β > 2, β - 1 \leq | B |, β - 1 ∣ | B |$ , write $c_{β, B} (w)$ for the observed scalar coefficient of a control word. Existence of a nonempty zero coefficient is equivalent to tag halting:

TagHaltsFrom (β, B) \Leftrightarrow \exists w \neq ε : c_{β, B} (w) = 0 .

The initial queue is obtained by removing the first $β - 1$ letters of B and appending b; the other rule is $b \mapsto b$ . The nine-dimensional construction additionally requires that B contain b. The universal source reduction produces bodies beginning with b and proves all these hypotheses for every input program.

The series reads the first coordinate after applying a control product to the paired boundary column. That column stores the fixed marker $M = 1 0^{β}$ as $c_{0} = {(μ, - 1, t, 0)}^{T}, μ = σ (M), t = 3^{| M |}$ , where σ is the ternary word value. The explicit four-dimensional matrices fix the coordinate convention used below.

Return families#

This is the single-cut specialization of interface compression.

Let A be a square transition, U an input map, and O an output map. The physical alphabet has only the transition and the cut C = UO. Runs of transitions between cuts expose the return matrices

M_{n} = O A^{n} U, n \in ℕ .

Return realizations let one binary matrix pair present a larger interface alphabet. The difficulty is the converse: arbitrary products may begin or end inside a transition run, and a pure power of A must not vanish.

Previous two-generator bound#

The complete prefix compiler gave two 10 × 10 integer matrices. Its word products span the full 10 × 10 matrix algebra, so every exact linear realization obtained by placing nonzero input and output maps around that family still needs ten dimensions. This obstructs exact realization of the old coefficient series, not replacement of its nonzero values. The construction below preserves exactly which words vanish while changing the other coefficients.

New Stuff#

Result#

Nine-dimensional mortality theorem. There is a primitive-recursive map from program codes to pairs of 9 × 9 integer matrices such that the emitted pair is mortal exactly when the program halts. Consequently M₉(2) is undecidable.

The reduction separates the inherited tag theorem from four new equivalences. In the diagram, $\tilde{G}$ is the four-matrix interface family consisting of the three paired controls and the new rank-one separator. The returns M_n realize that family using only two physical generators; hats denote their integer-scaled versions.

\begin{array}{rcll} CodeHalts (e) & \Leftrightarrow & TagHaltsFrom (β, B_{e}) & inherited \\ TagHaltsFrom (β, B_{e}) & \Leftrightarrow & HasNonemptyZero (c_{β, B_{e}}) & inherited \\ HasNonemptyZero (c_{β, B_{e}}) & \Leftrightarrow & IsMortal (\tilde{G}) & new \\ IsMortal (\tilde{G}) & \Leftrightarrow & IsMortal {M_{n} : n \in ℕ} & new \\ IsMortal {M_{n} : n \in ℕ} & \Leftrightarrow & IsMortal {A, UO} over ℚ & new \\ IsMortal {A, UO} over ℚ & \Leftrightarrow & IsMortal {\hat{A}, \hat{C}} over ℤ & new \end{array}

\begin{array}{rcl} CodeHalts & \leq_{0} & Mortality (9, 2), \\ \neg ComputablePred (Mortality (9, 2)) . \end{array}

Tilted separator#

Injective tilted code#

The nine-dimensional moment construction below selects the tail row up to a nonzero scale; the ratio of each of its three equal tail coordinates to its affine coordinate is q. The obligation here is to prove that this selected row has exactly the old zero set.

Let w_c be the lower word of the original c-rule tile, $1 H (B) 10$ , from the source table. Let V be its ternary value and $K = 3^{| w_{c} |}$ . The selected ratio and the new word code are

q = \frac{K - 3 V}{K - 3}, F_{q} (w) = ternaryCode (w) + q 3^{| w |} .

The restricted tag syntax gives q < −3/2. At this slope, words of different lengths occupy disjoint value bands; equal-length equality reduces to ordinary base-three injectivity. Lean proves tiltedTernaryCode_injective for all finite binary words and nearyTailRatio_lt_neg_three_halves for every encoded body.

Both paired phases#

The two paired phases differ only in where they store the lower-word coordinate. For upper word x and lower word y, put $h = σ (x) - σ (y)$ . Their columns are ${(h, - 3^{| y |}, 3^{| x |}, 0)}^{T}$ and ${(h, 0, 3^{| x |}, - 3^{| y |})}^{T}$ . Denote either column by v_phase(x,y). The row with three equal tail coefficients therefore gives

(1, q, q, q) v_{phase} (x, y) = F_{q} (x) - F_{q} (y) .

Its value is zero exactly when the upper and lower words agree. nearyTiltedPairedCoefficient_eq_zero_iff proves this for every control word and both phases. Put $u = T c_{0}$ . This separator column is the ordinary paired right boundary after one toggle, so its sandwiched coefficient on w is the tilted paired coefficient after appending that toggle. Zero-language equivalence therefore transfers every nonempty witness. With the existing boundary column u, the row defines the rank-one separator

\tilde{Π} = u (1, q, q, q) .

Nine-dimensional return realization#

Moment sequence#

We want waiting times zero, one and two to select the three paired controls, and every longer wait to select a nonzero multiple of the new separator. Thus the infinite return family will have only four effective choices.

To obtain that sequence, start with a one-dimensional geometric tail and extrapolate it backward to the first three times. Subtract these extrapolated values from T, D_b and D_c. The remaining sequence vanishes from time three onward. Its time-two residual has rank two, requiring two length-three nilpotent chains. After their time-one contribution is removed, a rank-one residual requires one length-two chain. The time-zero residual factors through those chain endpoints. Restoring the geometric eigenline gives $3 + 3 + 2 + 1 = 9$ dimensions.

The exact symbolic checker constructs this residual factorization. Lean verifies the resulting rational 9 × 9 transition A, 9 × 4 input U, 4 × 9 output O, and every moment identity:

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

Here s is nonzero and R is a nonzero scalar multiple of the tilted separator. The sparse transition and every rational entry of the larger U and O maps are explicit in ChangedSeparatorRealization. Separate theorems check zero_moment, moment_one, moment_two, and moment_add_three. The transition has block profile

A \sim J_{3} (0) \oplus J_{3} (0) \oplus J_{2} (0) \oplus [s] .

For β > 0 and b ∈ B, the realization denominators and basis pivots are nonzero. The universal source has β > 2 and emits every body beginning with b, so the chart is total on every emitted program.

Pure transition words#

Let e be the basis vector of the geometric tail. The transition acts on it by the nonzero eigenvalue s, so every power remains nonzero:

A e = s e, A^{n} e = s^{n} e \neq 0 .

Singular return compression#

The physical generators are A and the singular cut C = UO. The cut need not be invertible. The single-cut interface theorem, formalized as pairGenerator_isMortal_iff_returnFamily, assumes only that Aⁿ ≠ 0 for every n ∈ ℕ and gives an exact equivalence:

IsMortal {A, UO} \Leftrightarrow IsMortal {O A^{n} U : n \in ℕ} .

For the difficult direction, any physical zero containing a cut has a unique run form with exterior waits. Multiplying the entire zero on the left by O and on the right by U retains those waits as the first and last returns:

A^{p_{0}} UO A^{p_{1}} \dots UO A^{p_{r}} = 0 \Rightarrow (O A^{p_{0}} U) \dots (O A^{p_{r}} U) = 0 .

Conversely, cuts wrap any product of returns:

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

A physical zero without a cut would be a pure power of A, excluded by the eigenline. The displayed identity turns every zero product of returns into a physical zero with cuts. Thus arbitrary initial and terminal transition runs create no unproved exterior-cancellation case.

It remains to replace the infinite return alphabet by four interface generators. Lean proves each return has the form ρ_nG_ℓ(n), where ρ_n ≠ 0 and G ranges over T, D_b, D_c, and the tilted separator. The relabelling ℓ has the explicit right inverse selecting return times 0, 1, 2, and 3. Hence every four-generator interface word lifts to a return word, while any return word projects to an interface word. The corresponding products differ by the product of their nonzero return scalars, so zero products are preserved in both directions.

The four-generator interface family adjoins the rank-one tilted separator to the three paired controls. Its mortality is therefore zero reachability for the sandwiched tilted coefficient. Adjacent separators test the empty intervening control word; Lean proves that coefficient nonzero. The zero-language theorem, together with the appended-toggle identity, identifies every remaining zero with a nonempty zero of the original paired series.

IsMortal {A, UO} \Leftrightarrow \exists w \neq ε : c_{β, B} (w) = 0 .

Primitive-recursive integer construction#

Unreduced denominator clearing#

The final step returns from rational matrices to the integer inputs of mortality. Denominator clearing preserves all zero products. To make this an effective reduction, the rational formulas are evaluated as unreduced numerator-denominator pairs. Addition, multiplication, division, negation, and fixed powers remain primitive recursive without normalization or greatest-common-divisor computation. For each of the two labels, the 81 entries are flattened and cleared by one recursively accumulated common denominator. Effective is meant recursion-theoretically: Lean proves the assembled matrix-valued map primitive recursive; no extracted runtime artifact is asserted.

cast ({\hat{G}}_{i}) = d_{i} G_{i}, d_{i} \neq 0, {\hat{G}}_{i} \in M_{9} (ℤ) .

The two generators may use different factors. For an arbitrary nonempty label word, casting the integer product back to the rationals gives

cast ({\hat{G}}_{i_{1}} \dots {\hat{G}}_{i_{n}}) = (\prod_{j = 1}^{n} d_{i_{j}}) G_{i_{1}} \dots G_{i_{n}} .

Every d_i is nonzero, so the scalar product is nonzero in ℚ. The integer product is zero exactly when the rational product is zero. ChangedSeparatorEffectivity proves the scaling identity, mortality equivalence, and primitive recursiveness of every emitted entry.

Universal reduction#

CodeHalts(e) means that mathlib's universal partially recursive code e halts on input zero; this predicate is not computable. The fixed universal two-tag system is compiled through Cook's cyclic-tag construction and Neary's restricted binary-tag construction. Its width is greater than two; each constructed body is long enough, has length divisible by β − 1, begins with b, and is primitive recursive in e. The checked tag theorem identifies tag halting with CodeHalts(e).

CodeHalts (e) \Leftrightarrow TagHaltsFrom (β, b_{e}) \Leftrightarrow IsMortal ({\hat{G}}_{e}) .

mortality92Reduction combines that source map with the integer pair. Lean proves the resulting matrix-valued function primitive recursive, its mortality predicate equivalent to CodeHalts on every input, the many-one reduction, and noncomputability of M₉(2).

Consequences#

For every n ≥ 0, zero-block padding sends each 9 × 9 generator to

G_{i} \mapsto G_{i} \oplus 0_{n} .

The generic theorem isMortal_zeroPad_iff proves that this preserves and reflects every nonempty zero product. nearyMortality9Plus_primrec proves the padded coordinate family primitive recursive for every fixed n, and mortality9Plus_not_computable composes the reduction. Hence M_9+n(2) is undecidable for every n ≥ 0.

The subsequent M₈(2) construction preserves existence of a zero instead of the full zero language. nine_le_card_of_tilted_geometric_transfer_moments proves that the width-three bb benchmark already has transfer rank nine for every rational retuning of its one-mode geometric tail and every tilted ratio q < −3/2. This rules out direct parameter compression of the present chart, not the asymmetric existential construction in dimension eight.

Bookkeeping#

Verification and provenance#

Decision predicate

MortalityProblem.Mortal is mortality of a finite integer family under the nonempty-word convention.

Universal source contract

The contract owns primitive-recursive bodies, width, length, divisibility, leading-b, and exact halting hypotheses.

Zero-language-equivalent separator

tiltedTernaryCode_injective, the source ratio bound, and the paired-phase theorems establish the exact zero-language transport.

Nine-dimensional realization

The explicit realization and its moment modules check the 3+3+2+1 realization, first three returns, geometric tail, and total source locus.

Mortality equivalence

Return scaling, finite relabelling, singular-return compression, the pure-power guard, and zero-language transport compose here.

Effective integer pair

The realization is evaluated in primitive-recursive unreduced fractions; common-denominator clearing gives exact nonzero rational scalings.

Universal endpoint

mortality92Instance_primrec, codeHalts_reduces_mortality92, and mortality92_not_computable close dimension nine; mortality9Plus_not_computable closes every padded dimension.

Exact rank-nine benchmark

The checked compiler is identified with the benchmark moment family; a uniform 9 × 9 Hankel minor theorem excludes every eight-dimensional exact retuning in that family.

Transitive axioms

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

Formal scope#

Lean checks the source invariant, zero-language theorem for every control word, complete rational return family, arbitrary physical products, denominator clearing, primitive-recursive matrix entries, canonical Fin 2 instance, many-one reduction, and noncomputability conclusion. It also checks the primitive-recursive padded family and the composed endpoint in every dimension at least nine. The theorem does not depend on a finite search, floating-point computation, unproved invertibility, or an exterior-kernel assumption.

The exact symbolic checker separately reconstructs the realization as an exact cross-check, verifies its pivots and exterior identities, and certifies a rank-nine Hankel benchmark. The discovery audit records that calculation; its original list of remaining compiler obligations is superseded by the later Lean effectivity and undecidability modules.

Priority#

The project's public-literature search, last audited 24 July 2026, found no prior public proof of M₁₀(2) or M₉(2) before this series. The search covers publicly discoverable work, not unpublished results. Return realizations, rank-one separators, alphabet reduction, and rational denominator clearing are prior techniques. Priority is claimed for the nine-dimensional undecidability theorem and the complete construction assembled here, not for those inherited methods in isolation.

References#

GPT-5.6 Sol, elicited by @eternalism_4eva, Fixed-Boundary Correspondence, 2026. The restricted-tag source.
GPT-5.6 Sol, elicited by @eternalism_4eva, The Paired Scalar Series, 2026. The exact paired zero language and four-dimensional phase representation.
GPT-5.6 Sol, elicited by @eternalism_4eva, Binary Compilers, 2026. The previous M₁₀(2) bound and its public-literature audit.
Turlough Neary, Undecidability in Binary Tag Systems and the Post Correspondence Problem for Five Pairs of Words, STACS 2015. The restricted binary-tag source.
Julien Cassaigne, Vesa Halava, Tero Harju, and François Nicolas, Tighter Undecidability Bounds for Matrix Mortality, Zero-in-the-Corner Problems, and More, 2014. Prior bounds and standard transports.