Fixed-Boundary Correspondence

Known Stuff#

The definition of matrix mortality and the current bounded frontier are recorded on the series landing page.

Undecidability bounds#

For fixed dimension d and generator bound k, undecidability of M_d(k) is monotone in both coordinates: additional generators may be unused, and A ↦ A ⊕ 0 preserves mortality under dimension padding. The coordinatewise-minimal known undecidable cells therefore form an antichain.

Before this work, the best published antichain was [Cassaigne et al. 2014]

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

Cassaigne et al. also established the packing reduction

M_{d} (h k + 1) \leq_{m} M_{k d} (h + 1) .

Here ≤_m denotes a computable many-one reduction [Cassaigne et al. 2014]. This prior theorem propagates any new base case to other dimensions and generator counts.

Tag systems#

A tag system stores a finite word. A step reads its first symbol, appends the word assigned to that symbol, and deletes a fixed number β of leading symbols. It halts when fewer than β symbols remain. Halting is undecidable for Neary’s restricted binary family [Neary 2015].

Post correspondence#

A Post correspondence instance gives pairs of words (u_i, v_i). It asks for an index word i₁···i_n such that the upper and lower concatenations agree:

u_{i_{1}} \dots u_{i_{n}} = v_{i_{1}} \dots v_{i_{n}} .

For the pairs (a, ab) and (ba, a), the index word 12 is a solution because a·ba = ab·a.

Generalized PCP (GPCP) permits fixed boundary words [Nicolas 2008]. The instance used here has empty left boundaries and asks whether U(w)M = V(w) for a word w over four source letters.

The terminal-pair issue#

Neary’s five-pair construction used a fifth pair as a terminator [Neary 2015]. Rote identified an error in its terminal guard and proposed a longer replacement [Rote 2025]. Neither Neary’s terminal pair nor Rote’s replacement is used in the GPCP or mortality proof. A fresh-marker pair is introduced later only to obtain an ordinary five-pair PCP corollary.

The only external undecidability theorem imported below is Neary’s restricted tag-system undecidability. No PCP(4) theorem is assumed.

New Stuff#

GPCP(4), not PCP(4)#

The four simulation pairs from Neary’s refereed construction naturally finish with a controlled residual rather than equality [Neary 2015]:

U (w) M = V (w), M = 1 0^{β} .

Ordinary PCP accepts only U(w) = V(w), so a selectable pair must consume the final M. Neary’s published construction adds a fifth terminal pair. His 2013 preprint instead made an erasing pair participate in both simulation and termination [Neary 2013]. Because that pair remained selectable at every position, the converse had to exclude premature and repeated uses. The required arbitrary-word exclusion was not established, and PCP(4) was not retained in the refereed successor, which left the four-pair case open [Neary 2015].

GPCP makes M fixed punctuation rather than a selectable pair. It occurs once at the prescribed boundary while the four pairs perform only simulation. All eight morphism images remain nonempty. This proves GPCP(4), not PCP(4); ordinary PCP(4) remains unresolved in the literature audited here.

The new converse applies to arbitrary tile words. Zero-run synchronization forces one rule tile followed by exactly β−1 deletion tiles; each block decodes as a β-symbol tag stroke; global equality becomes a queue-history certificate; prefix cancellation reconstructs lawful tag steps until the first short queue. Malformed words are excluded by this global invariant, not by assuming that every wrong local choice eventually mismatches.

GPCP(4) is sufficient for mortality. Four payload matrices and one repeated rank-one boundary separator give M₃(5). Rank-one endpoint absorption is prior art [Halava–Harju–Hirvensalo 2007]; the new ingredient is the proved four-letter fixed-boundary source.

Result and consequences#

The source and matrix reductions below prove M₃(5). Substituting 5 = 2·2 + 1 and 5 = 1·4 + 1 into the established packing theorem gives M₆(3) and M₁₂(2); dimension padding gives the further consequences stated in the theorem box.

The series landing page owns the current frontier. This article records the theorem and its direct transports, not a snapshot of results established later.

A synchronized tag compiler#

Fix β ≥ 3 and a word q over b,c. Define the tag system

b \mapsto b, c \mapsto q b, I = {drop}_{β - 1} (q) b .

Encode queue letters and the fixed boundary by

H (b) = 1 0^{β} 1, H (c) = 1, M = 1 0^{β} .

Extend H by concatenation and define four word pairs:

Tile	Upper word	Lower word	Role
R_c	1	1 H(q) 1 0	apply the c-rule
R_b	1 0^β 1	1 1 0	apply the b-rule
D_c	1	0	erase one c
D_b	1 0^β 1	0	erase one b

For a tile word w, write U(w) and V(w) for its upper and lower concatenations.

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

The equivalence holds when β−1 divides |q| and |q| ≥ β−1. These hypotheses define an arithmetic envelope containing Neary’s compiler outputs.

Neary’s Table 2 supplies the historical design [Neary 2015]. The repository defines that compiler, proves its forward and arbitrary-execution converses, and constructs the padded output primitive recursively from mathlib’s code-halting source. No theorem from Neary’s terminal-pair argument is imported.

Padding into the arithmetic envelope

Neary has β = 10p and |qb| = βs. If n is the input length and r the maximum cyclic appendant length, take

B = \max {11 (n + p) + β - 2, 11 p, 11 r, 1}, x = ⌈ \frac{B - 1}{β - 1} ⌉, s = x (β - 1) + 1 .

This choice makes every variable exponent in Neary’s Table 2 nonnegative, so every specified track still has length s. Increasing s changes only the displayed padding and full copies of the program word. Because that word has length βs, adding full copies does not change the object-length or entry-shift residues modulo β used in Neary’s track-by-track simulation. Thus Table 2 remains valid for this choice. Moreover,

| q | = β [x (β - 1) + 1] - 1 = (x β + 1) (β - 1),

which implies β−1 ∣ |q| and |q| ≥ β−1.

Soundness for arbitrary tile words#

Assume U(w)M = V(w) for an arbitrary tile word w.

Synchronization

The upper side U(w)M is an H-encoded word followed by M. Every positive run of zeros therefore has length exactly β. On the lower side, a rule tile ends with one zero; an erase tile contributes one more; the next rule begins with a one.

The payload H(q) contains only complete β-runs and ends at a code boundary before the rule tile’s final 10. Hence every rule tile is followed by exactly β−1 erase tiles, and every matching word factors into blocks

R_{a_{0}} D_{a_{1}} \dots D_{a_{β - 1}},

one block for each length-β stroke a₀···a_β−1. The finite-state scan ranges over all label words; it assumes no simulated-history prefix.

History equation

Appending one final 1 turns the boundary M into the codeword H(b), so injectivity of H decodes the equality. The decoded equality forces the initial stroke to begin with c. If z denotes its remaining β−1 symbols, then z and q are prefixes of the same word. Because q has at least β−1 symbols, z is its length-(β−1) prefix. Cancel this initialization stroke. For the remaining stroke sequence S, let C(S) be its concatenation and P(S) the concatenation of the appendants selected by its stroke heads. The decoded equality becomes

C (S) b = I P (S) .

Here I is the initial queue defined above.

Execution

If the current queue has length at least β, it and the next stroke are prefixes of the same certified word. Since the stroke has length β, it equals the first β queue symbols. Delete the stroke, append the rule word selected by its head, cancel the common prefix, and iterate.

If the queue is shorter than β, the tag system has halted and the unused certificate suffix is irrelevant. Thus every history equation yields a genuine terminating execution.

Reusable source lemma#

For any deletion-width-β tag system, let S be a list of β-letter strokes, C(S) their concatenation, and P(S) the concatenation of the appendants selected by their heads. If

C (S) F = I P (S) and | F | < β,

then the tag system halts from I, by induction with prefix cancellation. To reuse the lemma, a word code must force candidate labels into strokes and decode equality into this certificate. The formal statement is tagHaltsFrom_of_history.

For the reverse implication, record the β symbols deleted at each tag step. Every reachable queue ends in b and has length 1 modulo β−1. A queue shorter than β is therefore exactly b. Reversing the cancellations constructs a matching tile word.

Additional corollary: corrected five-pair PCP#

An ordinary five-pair PCP instance is obtained by adjoining a fresh symbol # and the pair

(M #, #) .

Every ordinary upper image ends in 1 and every ordinary lower image ends in 0, so an ordinary-only word cannot solve PCP. At the first terminal pair, prefix compatibility of U(w)M# and V(w)# forces U(w)M = V(w). The prefix through that pair is already a solution. Hence a primitive solution, one not decomposable into two nonempty solutions, uses the terminal pair exactly once and last.

The fixed-length code 0↦00, 1↦01, #↦11 restores a binary target alphabet while preserving equality, prefix comparability, and primitivity.

More generally, if the ordinary pairs have no solution, the fixed-boundary equation U(w)s = V(w)t reduces to PCP by adjoining (s#, t#). Every primitive solution then uses the marked pair exactly once and last.

Fixed boundaries and rank one#

Recode binary symbols as nonzero ternary digits, 0↦1 and 1↦2. For a digit word x, let σ(x) be its base-three value. Nonzero digits make σ injective across words of unequal as well as equal length.

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

Direct multiplication gives:

Concatenation

Ψ (x x^{'}, y y^{'}) = Ψ (x, y) Ψ (x^{'}, y^{'})

Equality test

e_{1}^{T} Ψ (x, y) e_{3} = 0 \Leftrightarrow x = y

Nonsingularity

\det Ψ (x, y) = 3^{| x | + | y |} \neq 0

Let X₁, …, X₄ encode the four ordinary word pairs. With ε denoting the empty word, define X_★ = Ψ(M, ε) and

c = X_{★} e_{3}, A_{★} = c e_{1}^{T} = X_{★} e_{3} e_{1}^{T} .

The mortality family is {X₁, …, X₄, A_★}. Its ordinary generators are nonsingular and upper triangular. The third coordinate of c is 3^|M|, so A_★ is nonzero and has rank one.

Forward implication#

If w satisfies U(w)M = V(w), the corresponding matrix product X_w satisfies

A_{★} X_{w} A_{★} = c (e_{1}^{T} X_{w} X_{★} e_{3}) e_{1}^{T} = 0 .

The same generator supplies both rank-one factors; no separate boundary generator is required.

Converse for arbitrary products#

A product containing no A_★ is nonsingular. A product containing t copies has a unique decomposition

P_{0} A_{★} P_{1} A_{★} \dots A_{★} P_{t},

where every P_j is a possibly empty ordinary product. Expanding the rank-one factors gives

(P_{0} c) [\prod_{1 \leq j < t} e_{1}^{T} P_{j} c] (e_{1}^{T} P_{t}) .

The exterior column and row are nonzero because the ordinary blocks are nonsingular. For t = 1 the product is therefore nonzero. For t ≥ 2 it vanishes exactly when some internal scalar e₁^TP_jc vanishes. Writing P_j = X_w, the ternary equality test identifies this condition with U(w)M = V(w).

Reusable fixed-boundary compiler#

Let α be any finite source alphabet, let u, v: α → {0,1}^*, and fix right boundaries s, t. Put X_a = Ψ(u(a), v(a)), X_★ = Ψ(s, t), and A_★ = X_★e₃e₁^T. Then

{X_{a} : a \in α} \cup {A_{★}} is mortal \Leftrightarrow \exists w \in α^{*} : u (w) s = v (w) t .

The construction uses |α| ordinary generators and one rank-one generator. The fracture formula covers every product word; no witness normal form is assumed. Its machine-checked statement is absorbedFamilyInt_mortal_iff_terminal_match. Endpoint absorption is prior art [Halava–Harju–Hirvensalo 2007]; the new input is the four-letter fixed-boundary source.

Bookkeeping#

Verification and provenance#

Formalized reduction

The fixed universal source compiler, four-tile synchronization theorem, queue-history soundness, fresh-marker PCP repair, ternary representation, rank-one compiler, converse for every five-matrix word, and final no-decider theorem.

Transitive axioms

Lean reports propext, Classical.choice, and Quot.sound. The project contains no axiom declarations or admitted proofs.

Computable source reduction

Lean proves a primitive-recursive many-one reduction from mathlib’s code-halting predicate to the emitted five-matrix family and derives its no-decider theorem. Neary’s Lemma 9 is provenance, not a proof premise.

Finite falsifier

An independent program checked 20,272,272 bounded arbitrary tile words without finding a terminal-equation mismatch. This computation is not used in the proof.

Priority#

Neary’s one-version 2013 technical report claimed both four-pair PCP and M₃(5) [Neary 2013]. His refereed successor did not retain the four-pair theorem, explicitly left that case open, and proved only M₃(6) [Neary 2015]. Later literature retained the six-matrix bound [Bell–Potapov–Semukhin 2021] [Dong 2023]. No formal withdrawal is known.

The numerical statement is therefore prior. This proof establishes the fixed-boundary language of the four ordinary 2015 pairs and then applies rank-one endpoint absorption. No accepted proof of M₃(5) or binary-target GPCP(4) was found. The repository’s novelty audit records the search and qualification.

Complete source repositoryManuscript, Lean development, verification suite, falsifier, references, and version history

References#

Turlough Neary, Undecidability in Binary Tag Systems and the Post Correspondence Problem for Four Pairs of Words, arXiv:1312.6700v1, 2013. The earlier public M₃(5) claim, not retained in the refereed successor.
Turlough Neary, Undecidability in Binary Tag Systems and the Post Correspondence Problem for Five Pairs of Words, STACS 2015. The universal restricted 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. The previous undecidability antichain and packing reductions.
François Nicolas, (Generalized) Post Correspondence Problem and Semi-Thue Systems, 2008. The bounded-GPCP conventions and prior open cases.
Vesa Halava, Tero Harju, and Mika Hirvensalo, Undecidability Bounds for Integer Matrices Using Claus Instances, 2007. Prior rank-one endpoint absorption.
Günter Rote, Probabilistic Finite Automaton Emptiness Is Undecidable for a Fixed Automaton, MFCS 2025. Diagnosis of the terminal-pair flaw and the long-block proposal.
Paul C. Bell, Igor Potapov, and Pavel Semukhin, On the Mortality Problem, 2021. Later mortality bounds.
Ruiwen Dong, Recent Advances in Algorithmic Problems for Semigroups, 2023. Survey context.