Paired-Role Compression

Known Stuff#

The four-role source#

The fixed-boundary correspondence theorem proves undecidability of a four-role source problem.

Fix a deletion width β and write H for Neary’s binary word code, with H(b) = 10^β1 and H(c) = 1. For the variable part q of the c-appendant, the four ordinary roles are

\begin{array}{ll} R_{c} & = (1, 1 H (q) 10), \\ D_{c} & = (1, 0), \\ R_{b} & = (H (b), 110), \\ D_{b} & = (H (b), 0) . \end{array}

Let U(w) and V(w) be the upper and lower concatenations of a role word w, and put M = 10^β. The M₃(5) result proves

\exists w : U (w) M = V (w) \Leftrightarrow the associated restricted tag system halts.

The soundness proof analyzes every role word. Zero-run synchronization forces exact deletion-width blocks, and a global history equation reconstructs lawful tag steps. Neary’s restricted binary-tag undecidability theorem supplies the external source family [Neary 2015].

Neary padding corollary. Neary’s compiler has β = 10p and permits a computably chosen sufficiently large padding parameter s. Taking s = x(β−1)+1 makes the body length

| q | = β s - 1 = (x β + 1) (β - 1) .

β > 2, β - 1 \leq | q |, β - 1 ∣ | q | .

The padded subfamily remains undecidable. These conditions follow from the construction’s padding freedom, not from the bare statement of Lemma 9.

Word-pair matrices#

Recode binary symbols as nonzero base-three digits. For a digit word x, let σ(x) be its base-three value. The standard word-pair representation is

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

It is a monoid morphism, and its upper-right entry vanishes exactly when u = v [Cassaigne et al. 2014]. The M₃(5) construction assigns one such matrix to each role and one rank-one boundary matrix, giving five 3 × 3 generators.

Previous bounds#

After the M₃(5) result, the established Pareto-minimal mortality-undecidability points were

M_{3} (5), M_{5} (4), M_{6} (3), M_{12} (2) .

The four-generator entry M₅(4) came from earlier packing results. This result lowers its dimension by one.

New Stuff#

Result and mechanism#

The rule and deletion roles for a fixed tag symbol have the same upper word. After separating the upper and lower matrix channels, each pair therefore agrees on a two-dimensional subspace. Two three-dimensional phase spaces can be identified along that subspace, leaving four dimensions. A toggle selects which member of each pair acts. Every toggle pattern decodes to a role word, and every role word has an encoding.

Paired-role compression. Let V be a finite-dimensional vector space over a field, with dim V = d, and let R₀, R₁, D₀, D₁ be linear endomorphisms of V. If R_i and D_i agree on an r-dimensional subspace E for i = 0,1, then scalar zero reachability for the four actions reduces to scalar zero reachability for three actions in dimension 2d−r.

The Neary role matrices have d = 3 and r = 2. The compressed scalar system has three 4 × 4 matrices. A fourth rank-one matrix converts its zero coefficient into a zero matrix product.

The shared channel#

Side-normal form#

Use the unimodular change of basis

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

Conjugating Ψ separates the two word channels:

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

Agreement plane#

On the upper-side plane

E_{U} = span {e_{1}, e_{3}} = {(a, 0, z)^{T}},

the lower word disappears:

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

Since R_x and D_x have the same upper word,

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

Paired-role compression#

The quotient#

On two copies of the original space define

{\hat{G}}_{x} = [\begin{matrix} 0 & 0 \\ R_{x} & D_{x} \end{matrix}], \hat{T} = [\begin{matrix} 0 & I \\ I & 0 \end{matrix}] .

The subspace

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

is annihilated by both data matrices and preserved by the toggle. The three maps descend to

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

The row (ℓ^T, ℓ^T) annihilates K; the boundary column (c,0)^T descends without restriction. Thus the quotient preserves the required scalar coefficients.

Arbitrary control words#

The quotient matrices are indexed by two data letters and one toggle. Products are written in source-word order, but the rightmost matrix acts first on the boundary column. The decoder is therefore suffix-controlled: scan from right to left with a two-valued phase.

The initial phase is rule.
A toggle flips the phase.
A data letter x emits R_x in rule phase or D_x in deletion phase, then sets the phase to deletion.

Let τ(z) be the emitted role word in the original left-to-right order. Induction on z gives the coefficient identity

L G_{z} C = e_{1}^{T} X_{τ (z)} c .

Leading, trailing, adjacent, and repeated toggles are included. Conversely, induction on a role word inserts at most one toggle before each recursively encoded suffix, so τ is surjective. The scalar system has a zero witness exactly when the four-role source has one.

Explicit scalar system#

For x ∈ {b,c}, write

\begin{array}{lll} 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}

In quotient coordinates (p₁+q₁, p₂, p₃+q₃, q₂)^T, the matrices 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}] .

Let μ = σ(M) and t = 3^|M|. The boundary row and column are

L = (1, 0, 0, 0), C = (μ, - 1, t, 0)^{T} .

All entries are integers. Both data matrices have a zero second row; nonsingularity is not used. All three controls fix e₁, and T is a permutation matrix. A control word containing no data letter is a power of T and has coefficient LC = μ ≠ 0.

From a scalar zero to mortality#

Adjoin the outer product

S = C L = [\begin{matrix} μ & 0 & 0 & 0 \\ - 1 & 0 & 0 & 0 \\ t & 0 & 0 & 0 \\ 0 & 0 & 0 & 0 \end{matrix}] .

The vector C and row L are nonzero, so S is nonzero and has rank one over ℚ.

The outer-product reduction from scalar zero reachability to mortality is prior art [Cassaigne et al. 2014]. The new steps are the four-dimensional scalar system and the converse for a control family containing singular data matrices, using its common fixed column.

Forward implication#

If a control product Q satisfies LQC = 0, then

SQS = C (LQC) L = 0 .

Thus every fixed-boundary solution produces a mortality witness over {G_b, G_c, T, S}.

Arbitrary-product converse#

A product without S fixes e₁ and is therefore nonzero. A product with m ≥ 1 occurrences has a unique decomposition

Q_{0} S Q_{1} S \dots S Q_{m},

where each Q_i is a possibly empty control product. Expanding the outer products gives

(Q_{0} C) [\prod_{1 \leq i < m} L Q_{i} C] (L Q_{m}) .

The terminal row is nonzero because (LQ_m)e₁ = 1. If Q₀C = 0, then LQ₀C = 0 already supplies a scalar witness; an empty Q₀ cannot collapse the nonzero column C. Otherwise the exterior outer product is nonzero, so the full product vanishes only when an internal scalar LQ_iC vanishes. Empty internal blocks contribute LC = μ ≠ 0.

This covers one separator, adjacent separators, arbitrary exterior blocks, and every separator count. The argument uses the shared fixed column in place of control-matrix invertibility.

Consequences#

Here Z_d(k) asks, for supplied L and C, whether

L Y C = 0

for some nonempty product Y of at most k integer d × d matrices. The decorated form Z̊ requires every generator to have first column e₁. The empty product cannot witness this instance:

L C = μ \neq 0 .

The direct scalar construction proves Z̊₄(3) undecidable. Forgetting the restriction gives Z₄(3); the established reduction Z_d(k) ≤_m R_d+1(k) gives R₅(3) [Cassaigne et al. 2014].

The four-dimensional separator construction proves M₄(4). The series landing page records the current scalar, corner, and mortality frontiers.

Bookkeeping#

Verification and provenance#

Paired compression

Lean checks the side-normal conjugation, agreement plane, explicit matrices, coefficient identity for every control word, and decoder surjectivity.

Mortality equivalence

Lean checks every separator count and placement, the common-column converse with singular data controls, integer reflection, nonzeroness, and rational rank one.

Transitive axioms

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

Independent falsifier

A separate exact-arithmetic program checks bounded arbitrary role words, compressed coefficients, decoder coverage, and arbitrary four-matrix products. It is not used in the proof.

Formal scope#

The instance-level equivalence from the restricted tag semantics through the four exact integer matrices is machine-checked. The theorem nearyMortality44_mortal_iff_tagHaltsFrom is the encoded boundary.

Lean checks the explicit four-dimensional realization and its arbitrary-word identity. The abstract 2d−r quotient theorem above is paper mathematics, not a separate Lean declaration.

The computable reduction from mathlib’s code-halting predicate through the fixed universal machine, two-tag system, cyclic-tag system, and restricted binary-tag compiler is machine-checked. The four-matrix target equivalence is also machine-checked. A primitive-recursive declaration for this target constructor and its final many-one wrapper remain formalization debt; no external universality theorem is assumed. Frontier transports and bibliographic priority claims remain external to Lean.

Priority#

To our knowledge, after searches through 22 July 2026, no prior proof establishes M₄(4), nor scalar zero reachability for three 4 × 4 integer matrices sharing first column e₁. The closest CHHN bounds are M₅(4) and structured Z₅(3) [Cassaigne et al. 2014]. The anti-diagonal quotient is standard linear algebra, and the rank-one scalar-to-mortality separator is prior art; no source was found for the paired-role suffix decoder, the resulting four-dimensional scalar theorem, or the common-column mortality converse. “No prior art found” is limited to publicly discoverable work.

References#

GPT-5.6 Sol, elicited by @eternalism_4eva, Fixed-Boundary Correspondence, 2026. The synchronized four-role source theorem and five-matrix compiler.
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. Definitions, prior bounds, and the scalar-to-corner reductions.