The Paired Scalar Series

Fixed-boundary correspondence for Neary’s tag systems uses four word pairs, a rule tile and a deletion tile for each of two letters. Three integer 4 × 4 matrices, two data controls and a phase toggle, encode the same equality test: for every word z over the controls, the coefficient e₁^TG_zc vanishes exactly when the role word decoded from z solves the fixed-boundary equation, and every role word is decoded from some control word. The saving comes from a plane on which the rule and deletion matrices of each letter agree. Every exact linear representation of this series needs four dimensions; representations that only preserve which words give zero may be smaller.

The series is a scalar construction, not a mortality theorem. It is the source of M₄(4), Z₄(3), M₉(2), and M₈(2).

Known Stuff#

The four roles#

Fixed-boundary correspondence turns a run of a Neary tag system with width β and body B into a word equation. Its alphabet has four roles, the tiles R_x and D_x for each letter x ∈ {b, c}. For a role word w, U(w) and V(w) are the upper and lower concatenations, and M = 10^β is the fixed boundary word. Call the source admissible when

β \geq 3, | B | \geq β - 1, β - 1 ∣ | B | .

For admissible sources, some role word satisfies U(w)M = V(w) exactly when the tag system halts, and deciding this is therefore impossible in general. With the word-pair matrices X_a = Ψ(u_a, v_a), the equation is the scalar test e₁^TX_wΨ(M, ε)e₃ = 0. The empty role word gives σ(M) ≠ 0.

Separated coordinates#

Conjugating by the unimodular matrix

P = [\begin{matrix} 1 & 0 & 0 \\ 0 & 1 & 1 \\ 0 & 0 & 1 \end{matrix}]

puts the two words in separate coordinates:

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

The second coordinate carries the lower word and the third the upper word; the first accumulates the signed difference of their values. The row e₁^T is unchanged, and the boundary column becomes

P^{- 1} Ψ (M, ε) e_{3} = {(μ, - 1, t)}^{T}, μ = σ (M), t = 3^{| M |} .

From here on, R_x and D_x also denote the tiles’ matrices Φ(u, v) in these coordinates.

Hankel rank#

A scalar function f on words has a linear representation of dimension n if f(w) = λY_wγ for a row λ, a column γ, and n × n matrices Y_a for the letters. Its Hankel matrix has entries f(xy) indexed by words x, y. Since f(xy) = (λY_x)(Y_yγ), the Hankel matrix factors through an n-dimensional space, so any m × m submatrix with nonzero determinant proves n ≥ m.

New Stuff#

Result#

A role is a letter together with a phase, rule or deletion. The paired series moves the phase from the alphabet into the state. The current vector lives in one of two copies of the three-dimensional space, one copy per phase. A data letter x applies R_x or D_x according to the copy it finds the vector in and leaves the result in the deletion copy, and the toggle moves the vector to the other copy. This uses three generators in dimension six. For each letter, R_x and D_x have the same upper word, so they agree on the plane of vectors whose lower-word coordinate is zero, and the two copies may share that plane. Identifying them there leaves dimension 6 − 2 = 4.

Theorem (paired-role compression). Let V be a d-dimensional vector space over a field, let R₀, R₁, D₀, D₁ be endomorphisms of V, and suppose R_i and D_i agree on an r-dimensional subspace E for i = 0, 1. For every row ℓ and column γ there are three endomorphisms of a (2d−r)-dimensional space, a row, a column, and a surjective decoder τ from control words to role words such that every control word z has coefficient ℓX_τ(z)γ.

Theorem (paired scalar series). For every admissible source, the integer 4 × 4 matrices G_b, G_c, T and the column c = (μ, −1, t, 0)^T below satisfy, for every word z over {G_b, G_c, T},

e_{1}^{T} G_{z} c = σ (U (τ (z)) M) - σ (V (τ (z))) .

Hence some nonempty control word has coefficient zero exactly when the tag system halts. Every exact linear representation of this function of z over ℚ has dimension at least four.

The coefficient e₁^TG_zc is the paired coefficient of z. Toggle-only words decode to the empty role word and have coefficient μ ≠ 0, so they never give a spurious zero.

The agreement plane#

On the plane E = span{e₁, e₃}, where the lower-word coordinate is zero, the lower word has no effect:

Φ (u, v) {(a, 0, z)}^{T} = {(a + σ (u) z, 0, 3^{| u |} z)}^{T} .

The tiles R_x and D_x have the same upper word, H(x), so

R_{x} |_{E} = D_{x} |_{E} (x \in {b, c}) .

The phase quotient#

On V ⊕ V, the first summand holds a vector in rule phase and the second a vector in deletion phase. Define

{\hat{G}}_{x} (p, q) = (0, R_{x} p + D_{x} q), \hat{T} (p, q) = (q, p) .

Starting from (γ, 0), the vector always lies in one summand, and a data letter applies the tile of the phase it finds. Because R_x and D_x agree on E, both data maps kill the anti-diagonal

K = {(p, - p) : p \in E},

and the toggle maps K to itself. All three maps therefore descend to the quotient

W = (V \oplus V) / K, \dim W = 2 d - r .

The boundary row (ℓ, ℓ) reads the sum of the two summands, so it vanishes on K and descends as well; the column is the class of (γ, 0). Passing to the quotient therefore changes no coefficient. This proves the compression theorem, with the decoder described below.

Explicit matrices#

For the four roles, d = 3 and r = 2. Use the quotient coordinates

(p, q) \mapsto {(p_{1} + q_{1}, p_{2}, p_{3} + q_{3}, q_{2})}^{T} :

the difference and the upper word are shared, and the lower word sits in coordinate two in rule phase and in coordinate four in deletion phase. Let u_x = H(x) be the common upper word of the tiles for x, and v_x^R, v_x^D their lower words. Write

\begin{array}{ll} U_{x} = σ (u_{x}), & A_{x} = 3^{| u_{x} |}, \\ V_{x}^{R} = σ (v_{x}^{R}), & B_{x}^{R} = 3^{| v_{x}^{R} |}, \\ V_{x}^{D} = σ (v_{x}^{D}), & B_{x}^{D} = 3^{| v_{x}^{D} |} . \end{array}

These are numbers, not further generators. The quotient maps are

G_{x} = [\begin{matrix} 1 & V_{x}^{R} & U_{x} & V_{x}^{D} \\ 0 & 0 & 0 & 0 \\ 0 & 0 & A_{x} & 0 \\ 0 & B_{x}^{R} & 0 & B_{x}^{D} \end{matrix}], T = [\begin{matrix} 1 & 0 & 0 & 0 \\ 0 & 0 & 0 & 1 \\ 0 & 0 & 1 & 0 \\ 0 & 1 & 0 & 0 \end{matrix}],

with boundary row e₁^T = (1, 0, 0, 0) and boundary column c = (μ, −1, t, 0)^T, the separated boundary column placed in rule phase. All entries are integers. The toggle is a permutation matrix exchanging coordinates two and four. Both data matrices have zero second row, so they are singular. All three matrices have first column e₁.

Decoding every control word#

In a product G_zc the rightmost letter of z acts first. The decoder τ therefore reads z from right to left, starting in rule phase:

a toggle switches the phase;
a data letter x emits R_x in rule phase and D_x in deletion phase, and then sets the phase to deletion.

τ(z) is the emitted role word in left-to-right order. For example, G_bG_c decodes to D_bR_c, and G_bG_cT to D_bD_c. Induction on z proves the coefficient identity of the theorem for every control word, including words with leading, trailing, adjacent, or repeated toggles. Conversely, a role word is encoded from right to left: each role becomes its data letter, with a toggle immediately to its right exactly when the current phase differs from the role’s phase. Hence τ is surjective, and the empty role word is τ(T).

The two alphabets are different: a control word and its decoded role word have different letters and lengths. Only the existence of a zero transfers, and it transfers in both directions.

The two phase columns#

For a control word z, put X = U(τ(z))M, Y = V(τ(z)), and h = σ(X) − σ(Y). The whole column, not only its first coordinate, is determined by X, Y, and the final phase:

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

The paired coefficient reads only h, which vanishes exactly when X = Y. A different boundary row may also read the length coordinates; the two-generator constructions use this freedom.

Exact dimension#

Take the control-word prefixes ε, b, bb, bT and suffixes ε, T, b, bT, where b stands for G_b. The corresponding 4 × 4 section of the Hankel matrix is the product of a matrix of reachable rows and a matrix of observable columns, and both determinants are nonzero for every β ≥ 3 and every body. Every exact linear representation of the paired series over ℚ therefore has dimension at least four, and the quotient attains it. A representation that only needs the same zero set is not bound by this argument.

Dependents#

M₄(4) adds the rank-one separator ce₁^T to the three matrices; the three matrices alone give Z₄(3).
The six-dimensional scalar compiler spells the four roles in two bits and shares the upper-word coordinates between unfinished codewords.
M₉(2) and M₈(2) replace the boundary row by rows that also read the length coordinates, then realize the three controls and a rank-one separator as the returns of two matrices.

Bookkeeping#

Verification and provenance#

Four-dimensional realization

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

Exact dimension

Lean checks the Hankel factorization, both determinants, and the lower bound paired_exact_state_lower_bound.

Undecidability of the zero set

Lean proves that existence of a nonempty control word with zero paired coefficient is equivalent to code halting and is not a computable predicate.

Transitive axioms

The publication-facing declarations use only propext, Classical.choice, and Quot.sound.

Formal scope#

The explicit matrices, the coefficient identity for every control word, decoder surjectivity, the undecidability of the zero set, and the dimension lower bound are machine-checked. The general (2d−r)-dimensional compression theorem is proved on this page and has no separate Lean declaration; only its instance is formalized.

References#

GPT-5.6 Sol, elicited by @eternalism_4eva, M₃(5): Mortality of Five 3 × 3 Integer Matrices, 2026. Fixed-boundary correspondence.
GPT-5.6 Sol, elicited by @eternalism_4eva, M₄(4): Mortality of Four 4 × 4 Integer Matrices, 2026. The first publication of the paired construction.
Julien Cassaigne, Vesa Halava, Tero Harju, and François Nicolas, Tighter Undecidability Bounds for Matrix Mortality, Zero-in-the-Corner Problems, and More, 2014. Word-pair matrices.