The Paired Scalar Series

Verdict

Starting from four word-pair actions, we encode their word-equality test using three integer matrices of dimension four. Two matrices select a data letter; the third switches between rule and deletion phases. Every control word is decoded, not just encodings of intended computations.

This is a scalar-zero construction, not yet a mortality theorem: one observed coefficient must vanish. It is reused by M₄(4), M₉(2), and M₈(2). Four dimensions are necessary to preserve this exact series, but not necessarily its zero language alone.

Known Stuff#

Fixed-boundary source#

The four-tile construction turns a tag computation into a word-equality problem. Its alphabet has four roles: rule and deletion actions for each letter in {b, c}. A role word selects word pairs in order. Write U and V for their upper and lower concatenations and M for the fixed terminal marker. Acceptance means

U (w) M = V (w) .

The source parameters are a deletion width β and a binary body B. Here “admissible” means $β > 2, β - 1 \leq | B |, β - 1 ∣ | B |$ . For the emitted sources, a nonempty accepted role word exists exactly when the tag computation halts. We retain that equivalence while replacing four role labels by three controls.

Word-pair matrices#

Recode the source bits as nonzero ternary digits; write σ for the resulting word value. The word-pair representation assigns each pair (u, v) a 3 × 3 matrix Ψ. Matrix multiplication represents concatenation, and its upper-right entry is zero exactly when the words agree.

A unimodular basis change gives the following equivalent coordinates. The second column carries the lower word and the third the upper word; “channel” refers to those coordinates:

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

Let R_x and D_x be the rule and deletion matrices in these coordinates. For a fixed letter, the two roles have the same upper word. On the plane $E = span {e_{1}, e_{3}}$ , the lower-word column is unused, so the two matrices agree. This is the space we can share between phases.

New Stuff#

Result#

Paired scalar series. For every admissible source, let G_b, G_c be the two data matrices and T the toggle. Write G_z for their ordered product on a control word z. There are an integer boundary row r^T and column c such that the word series is

p_{β, B} (z) = r^{T} G_{z} c,

and p_β,B(z) = 0 exactly when the decoded role word satisfies the fixed-boundary equation. The equivalence holds for every raw control word, including arbitrary toggles.

Phase quotient#

A phase records whether the next data letter, acting on a column, selects a rule or a deletion. Before compression, store one copy of the word-pair vector for each phase. On their direct sum the data action and toggle are

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

Write V for the original three-dimensional space. The data actions send a difference between the two copies of E to zero, because the rule and deletion agree there. Thus the anti-diagonal subspace

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

is killed by both data controls and preserved by the phase toggle. All three maps descend to the quotient

W = (V \oplus V) / K, \dim W = 2 \cdot 3 - 2 = 4 .

The boundary row reads the sum of the two copies, so it annihilates K: identifying vectors differing by K cannot alter the coefficient. The boundary column starts in rule phase. The explicit integer matrices and boundary vectors implement this quotient; the general quotient argument works in dimension $2 d - r$ , where d is the original dimension and r the agreement dimension.

Complete decoder#

Matrix products act on the boundary column from right to left. The decoder therefore scans a control word from its suffix. It begins in rule phase; a toggle exchanges phases; a data letter emits its rule or deletion role according to the current phase and then enters deletion phase.

For example, the control word bc decodes to $D_{b} R_{c}$ : the rightmost c acts in rule phase and leaves deletion phase for b. A trailing toggle changes which role that c selects. Induction proves coefficient preservation for every control word. Conversely, inserting toggles gives a control spelling for every role word. These are different alphabets, linked by the decoder; existence of a nonempty zero is equivalent on the two sides.

Exact dimension#

Four explicit prefixes and four explicit suffixes form a 4 × 4 finite Hankel section with nonzero determinant for every admissible source. Any exact linear representation of this scalar series over ℚ therefore has at least four dimensions. The quotient construction has dimension four, so its realization dimension is exact.

Dependents#

The four-matrix mortality construction uses the four-dimensional matrices directly and adds a rank-one separator.
The shared-partial compiler binary-encodes the four source roles while retaining a common unfinished word channel.
The tilted separator changes nonzero coefficients without changing this series’ zero language, enabling a nine-dimensional return realization.
The asymmetric separator preserves only existence of a zero, replacing discarded witnesses by a leading toggle and permitting eight dimensions.

Bookkeeping#

Verification and provenance#

Four-dimensional realization

Lean checks the quotient coordinates, explicit matrices, decoder, coefficient identity, and surjectivity.

Exact rank

Lean checks the finite Hankel factorization, both determinant certificates, the four-dimensional lower bound, and attainment by the native representation.

Universal zero language

Lean proves that existence of a nonempty paired zero is exactly 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, every-word decoder identity, decoder surjectivity, exact zero-language theorem, universal source reduction, and state lower bound are machine-checked. The page introduces no approximation, intended-language restriction, or finite-word premise.

References#

GPT-5.6 Sol, elicited by @eternalism_4eva, Fixed-Boundary Correspondence, 2026. The four-role source zero language.
GPT-5.6 Sol, elicited by @eternalism_4eva, Paired-Role Compression, 2026. The explicit quotient matrices and mortality application.
Julien Cassaigne, Vesa Halava, Tero Harju, and François Nicolas, Tighter Undecidability Bounds for Matrix Mortality, Zero-in-the-Corner Problems, and More, 2014. Standard word-pair matrices.