Z₆(2) and M₁₀(2): Binary Compilers

Scalar zero reachability for two 6 × 6 integer matrices and matrix mortality for two 10 × 10 integer matrices are undecidable: Z₆(2) and M₁₀(2).

The scalar result holds when the matrices share first column e₁, under both the free-monoid and nonempty free-semigroup conventions. Consequently R₇(2) is undecidable.

Zero-block padding extends the mortality result to M_d(2) for every d ≥ 10.

The scalar theorem remains a frontier result. The mortality bound is now subsumed by M₈(2); this article retains its different prefix-decoder construction.

Known Stuff#

Four-role fixed-boundary family#

The shared input is the four-role fixed-boundary family: the tiles R_x, D_x for each letter x ∈ {b, c}. Write X_w for the product of their word-pair matrices along a role word w. With the boundary column c below, the fixed-boundary equation is equivalent to

e_{1}^{T} X_{w} c = 0 .

Deciding whether such a role word exists is undecidable. The four tile matrices are nonsingular; adjoining the rank-one separator gives the five matrices of M₃(5).

In the separated coordinates below, the boundary column is $c = {(μ, - 1, t)}^{T}, μ = σ (M), t = 3^{| M |}$ , where M is the boundary word and σ the ternary value.

Shared channel#

The separated coordinates write every word-pair matrix as

Φ (u, v) = (\begin{matrix} 1 & σ (v) & σ (u) \\ 0 & 3^{| v |} & 0 \\ 0 & 0 & 3^{| u |} \end{matrix}) .

For each letter x, the tiles R_x and D_x have the same upper word u_x, so their matrices agree on the plane where the lower-word coordinate is zero:

E = span {e_{1}, e_{3}}, R_{x} | E = D_{x} | E .

The paired scalar series shares this plane between the rule and deletion phases. The compilers below share it between the states of a binary decoder.

Previous binary bounds#

Cassaigne, Halava, Harju, and Nicolas established Z₉(2), R₁₀(2), and M₁₅(2), together with general alphabet-packing and scalar-to-corner reductions [Cassaigne et al. 2014]. The fixed-boundary result and their mortality packing give M₁₂(2). Binary codes and decoders that remember an unfinished codeword are prior techniques; the constructions below use the agreement plane to remove coordinates from the corresponding generic decoders.

New Stuff#

Results#

Generator packing reaches two generators by spelling each original matrix in a binary prefix code and keeping one copy of the space for every unfinished prefix, so each unfinished prefix costs a full copy. Both compilers here pay less, using the agreement plane.

The scalar compiler spells the four roles as two-bit words, phase bit first. A generic decoder keeps three copies of the three-dimensional space, for the unfinished prefixes ε, 0, 1, and needs nine coordinates. After the phase bit, the rule and deletion states differ only in their lower-word coordinate, and every state shares the difference coordinate, so six coordinates suffice.

The mortality compiler spells the five matrices of M₃(5) in a complete prefix code with four unfinished prefixes, which gives twelve dimensions. The agreement plane forces both generators to map into a common ten-dimensional subspace. Restricting to that subspace can create new zero products, but one extra letter at the end of a word maps any such product back to a zero of the twelve-dimensional pair.

Theorem (Z₆(2)). A primitive-recursive map sends every program to two 6 × 6 integer matrices with common first column e₁, an integer row, and an integer column such that some product of the matrices has zero coefficient exactly when the program halts. The statement holds whether or not the empty product is admitted. Hence Z̊₆(2), Z₆(2), and R₇(2) are undecidable.

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

Six-dimensional scalar compiler#

Two-bit code#

For each letter x, let u_x be the common upper word, and v_x^R, v_x^D the lower words of R_x and D_x.

Every binary pair denotes one role:

\begin{array}{rcl} 00 & \mapsto & R_{b}, \\ 01 & \mapsto & R_{c}, \\ 10 & \mapsto & D_{b}, \\ 11 & \mapsto & D_{c} . \end{array}

The numbers U_x, A_x, V_x^R, B_x^R, V_x^D, B_x^D are the ternary values and length powers of these words, as in the paired matrices.

Generators#

At a codeword boundary we need three coordinates: affine value a, lower component λ, and upper component υ. After the first bit, the rule/deletion lower components must be kept apart, but the unfinished upper component and affine value can be shared. This gives six row coordinates $(a, λ, υ, λ_{R}, υ_{*}, λ_{D})$ , with integer transition matrices

N_{0} = (\begin{matrix} 1 & 0 & 0 & 0 & 0 & 0 \\ 0 & 0 & 0 & 1 & 0 & 0 \\ 0 & 0 & 0 & 0 & 1 & 0 \\ V_{b}^{R} & B_{b}^{R} & 0 & 0 & 0 & 0 \\ U_{b} & 0 & A_{b} & 0 & 0 & 0 \\ V_{b}^{D} & B_{b}^{D} & 0 & 0 & 0 & 0 \end{matrix}),

N_{1} = (\begin{matrix} 1 & 0 & 0 & 0 & 0 & 0 \\ 0 & 0 & 0 & 0 & 0 & 1 \\ 0 & 0 & 0 & 0 & 1 & 0 \\ V_{c}^{R} & B_{c}^{R} & 0 & 0 & 0 & 0 \\ U_{c} & 0 & A_{c} & 0 & 0 & 0 \\ V_{c}^{D} & B_{c}^{D} & 0 & 0 & 0 & 0 \end{matrix}) .

The transition identities below explain the sparse entries: one bit stores the phase; the next applies its selected word-pair matrix and returns to a codeword boundary.

Arbitrary binary words#

For a row triple q = (a, λ, υ), put

\begin{array}{rcl} ι (q) & = & (a, λ, υ, 0, 0, 0), \\ ι_{R} (q) & = & (a, 0, 0, λ, υ, 0), \\ ι_{D} (q) & = & (a, 0, 0, 0, υ, λ) . \end{array}

Direct multiplication gives

\begin{array}{ll} ι (q) N_{0} = ι_{R} (q), & ι (q) N_{1} = ι_{D} (q); \\ ι_{R} (q) N_{x} = ι (q X_{R, x}^{T}), & ι_{D} (q) N_{x} = ι (q X_{D, x}^{T}) . \end{array}

Parse a binary word from the left into complete pairs and discard one final bit when the length is odd. If the pairs decode as a₁, …, a_n, define τ(z) = a_n⋯a₁. The reversal accounts for the transposed row action. With

L_{6} = (μ, - 1, t, 0, 0, 0), C_{6} = e_{1},

the transition identities give, for every binary word,

L_{6} N_{z} C_{6} = e_{1}^{T} X_{τ (z)} c .

An unpaired final bit changes only the unfinished phase and preserves the extracted first coordinate. Conversely, encoding the reversed sequence of any role word gives a binary preimage. The decoder is total and surjective.

Structured form#

Transposing both generators makes their first column e₁. Product reversal is a bijection on binary words, so scalar zero reachability is unchanged. The empty and one-bit coefficients equal μ ≠ 0; the free-monoid and nonempty free-semigroup conventions therefore agree. This proves structured Z̊₆(2), hence Z₆(2). The standard integral scalar-to-corner lift gives R₇(2) [Cassaigne et al. 2014].

Ten-dimensional mortality compiler#

Complete prefix code#

Transpose the normalized five-matrix family and write its rank-one separator as Π = e₁c^T. Denote the four payloads by R_c, R_b, D_c, D_b. For every p in the upper plane E,

p^{T} R_{x} = p^{T} D_{x} .

Use the complete prefix code

\begin{array}{rcl} 0 & \mapsto & Π, \\ 100 & \mapsto & R_{c}, \\ 101 & \mapsto & R_{b}, \\ 110 & \mapsto & D_{c}, \\ 111 & \mapsto & D_{b} . \end{array}

Its proper-prefix states are ε, 1, 10, and 11.

These are the prefixes at which reading may pause before recognizing a complete codeword. Each must carry a three-dimensional payload vector, initially giving twelve dimensions.

Twelve-dimensional realization#

Order four three-dimensional blocks by those prefix states. The binary generators are

𝒜_{0} = (\begin{matrix} Π & 0 & 0 & 0 \\ 0 & 0 & I & 0 \\ R_{c} & 0 & 0 & 0 \\ D_{c} & 0 & 0 & 0 \end{matrix}), 𝒜_{1} = (\begin{matrix} 0 & I & 0 & 0 \\ 0 & 0 & 0 & I \\ R_{b} & 0 & 0 & 0 \\ D_{b} & 0 & 0 & 0 \end{matrix}) .

Each block row contains one nonzero block. For every start state and binary word, its product therefore has one possibly nonzero block in that row: the deterministic final prefix state selects the column, and the emitted payload product is the block value. This covers complete codewords, unfinished suffixes, and every starting prefix state.

Synchronizer#

A zero decoded from the root state is not yet a zero of the whole block matrix: every other starting state must vanish too. A synchronizing word first brings all those states to the same codeword boundary.

The word 00 sends every prefix state to ε. Its four emitted products are

\begin{aligned} ε : & Π^{2}, \\ 1 : & R_{c}, \\ 10 : & R_{c} Π, \\ 11 : & D_{c} Π . \end{aligned}

If a role word w has zero matrix product, then 00 followed by its prefix encoding makes every block row zero. Conversely, a zero binary product has a zero root block, whose emitted payload product cannot be empty because the empty product is the identity. Thus the twelve-dimensional pair is mortal exactly when the five-matrix family is mortal.

Common-image restriction#

For p ∈ E, define the row ℓ_p = (0, 0, p^T, −p^T) in the four prefix blocks. Paired-role agreement gives

ℓ_{p} 𝒜_{0} = ℓ_{p} 𝒜_{1} = 0 .

The independent choices p = e₁, e₃ place both images in the ten-dimensional subspace

K = \ker ℓ_{e_{1}} \cap \ker ℓ_{e_{3}} .

A vector in K has block coordinates

(x_{1}, x_{2}, x_{3} | y_{1}, y_{2}, y_{3} | z_{1}, z_{2}, z_{3} | z_{1}, z_{4}, z_{3}) .

Let J embed the ten displayed coordinates into this vector, and let Q extract them, so QJ = I₁₀. Define

ℬ_{i} = Q 𝒜_{i} J (i \in {0, 1}) .

The coordinates are integral. Since each image lies in K,

𝒜_{i} J = J ℬ_{i} .

Mortality converse#

If a twelve-dimensional product 𝒜_z is zero, then ℬ_z = Q𝒜_zJ = 0. Conversely, if ℬ_z = 0, then 𝒜_z kills K. Because the image of 𝒜₀ lies in K,

𝒜_{z} 𝒜_{0} = 𝒜_{z 0} = 0 .

The appended letter converts every zero introduced by restriction into a zero of the twelve-dimensional decoder, which in turn yields a nonempty zero payload product. Hence the two 10 × 10 integer matrices are mortal exactly when the restricted tag system halts.

Consequences#

The six-dimensional construction proves the scalar and corner bounds Z₆(2) and R₇(2). The ten-dimensional construction proves M₁₀(2), now subsumed by the later eight-dimensional theorem. For every n ≥ 0,

ℬ_{i} \mapsto ℬ_{i} \oplus 0_{n}

preserves zero products, proving M_10+n(2). The decidability table records the current frontier.

Bookkeeping#

Verification and provenance#

Six-dimensional compiler

Lean checks the explicit generators, every binary word, odd residues, coefficient preservation, decoder surjectivity, and common-first-column transport.

Prefix transducer

Lean proves the arbitrary-word block-row theorem used by the complete prefix decoder.

Ten-dimensional compiler

Lean checks synchronization, twelve-dimensional mortality, the common image, integral restriction, the appended-letter converse, and zero padding.

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 proves the complete instance-level equivalences. The canonical declarations are nearyScalarZero62_hasZero_iff_tagHaltsFrom, nearyScalarZero62_hasZeroStar_iff_tagHaltsFrom, nearyMortality102_mortal_iff_tagHaltsFrom, and nearyMortality10Plus_mortal_iff_tagHaltsFrom.

The computable reduction from mathlib’s code-halting predicate to the restricted binary-tag system is machine-checked; Neary’s construction is provenance rather than an imported theorem [Neary 2015]. Lean proves both target constructors primitive recursive, the reductions codeHalts_reduces_scalarZero62 and codeHalts_reduces_mortality102, and the corresponding noncomputability theorems. The R₇(2) transport and bibliographic priority claims remain outside Lean.

Priority#

To our knowledge, after public-literature searches through 24 July 2026, no prior proof establishes Z₆(2), R₇(2), or M₁₀(2). CHHN’s corresponding established bounds are Z₉(2), R₁₀(2), and M₁₅(2) [Cassaigne et al. 2014]. Prefix coding, alphabet reduction, and scalar-to-corner transport are prior art. No source was found for the shared dimension-six partial channel or the ten-dimensional common-image restriction and its appended-letter mortality converse. “No prior proof found” is limited to publicly discoverable work.

References#

GPT-5.6 Sol, elicited by @eternalism_4eva, Fixed-Boundary Correspondence, 2026. The four-role fixed-boundary family.
GPT-5.6 Sol, elicited by @eternalism_4eva, The Paired Scalar Series, 2026. The shared source-recognition representation.
Turlough Neary, Undecidability in Binary Tag Systems and the Post Correspondence Problem for Five Pairs of Words, STACS 2015. The restricted binary-tag undecidability 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.
Günter Rote, Probabilistic Finite Automaton Emptiness Is Undecidable for a Fixed Automaton, MFCS 2025. Related binary prefix decoding with explicit treatment of unfinished codewords.