Orientation#

This glossary defines the vocabulary of the matrix-mortality series. It assumes undergraduate linear algebra and algebra and a first course in computability, including decidability, reductions, and Post’s correspondence problem, and defines what goes beyond them. Entries are grouped by subject; the index is alphabetical.

Notation#

Symbols below keep one meaning throughout the series. Symbols defined inside a single article are local to it.

Problems and decidability#

Semidecidable#

A problem is semidecidable if some algorithm halts and accepts on every yes-instance, possibly running forever on no-instances. Mortality is semidecidable: enumerating products by length finds a zero product whenever one exists. Undecidability of mortality is therefore the impossibility of recognizing every immortal family.

Primitive-recursive reduction#

A many-one reduction whose instance map is primitive recursive, a class of total computable functions built from basic functions by composition and bounded recursion. Every reduction to a mortality problem in this series is primitive recursive and is checked as such in Lean.

Matrix mortality#

Given finitely many square matrices of one dimension, the question whether some nonempty product of them is the zero matrix. A family with such a product is mortal; otherwise it is immortal. Entries are integers unless another ring is stated.

Bounded matrix mortality#

M_d(k) is matrix mortality for at most k integer d × d matrices. The parameters bound the family, not the entries or the length of the product.

Mortality witness#

A nonempty word over the generators whose product is zero, also called a zero word. The empty word is excluded because its product is the identity.

Scalar zero reachability#

Z_d(k) supplies a row L, a column C, and at most k integer d × d matrices, and asks whether LYC = 0 for some nonempty product Y. Only one coefficient must vanish. The structured form Z̊_d(k) requires every generator to have first column e₁.

Zero-in-the-corner problem#

R_d(k) is scalar zero reachability with L and C fixed to coordinate vectors: whether a designated entry of some nonempty product is zero. Z_d(k) reduces to R_d+1(k).

Parameter monotonicity and padding#

Undecidability of M_d(k) implies undecidability for every larger d and k: extra generators may go unused, and replacing each matrix A by A ⊕ 0 preserves and reflects every zero product.

Frontier antichain#

The minimal undecidable cells under the coordinatewise order. By monotonicity they determine every undecidable cell that is known; they say nothing about the cells below them.

Words and machines#

Word product and product order#

For a family indexed by letters, the product along a word w = w₁⋯w_n is taken in the written order, X_w = X_w1⋯X_wn. Applied to a column, the rightmost factor acts first; decoders in this series therefore read words from right to left.

Prefix code#

A set of codewords none of which is a proper prefix of another, so that a stream can be decoded from left to right without separators. It is complete when every infinite stream begins with a codeword.

Decoder#

A finite-state device that reads a coded word and emits source letters. A matrix compiler realizes one with block matrices: the block position stores the decoder state, such as an unfinished codeword or a phase, and the block value stores the product emitted so far.

Post correspondence problem#

PCP(n) gives n word pairs and asks for a nonempty index word whose upper and lower concatenations agree.

Generalized Post correspondence problem#

GPCP(n) additionally fixes boundary words that occur once, at the ends. The count n counts the selectable pairs, not the boundary.

Fixed-boundary correspondence#

The GPCP instance of this series: four word pairs, empty left boundaries, and the upper right boundary M, so a solution satisfies U(w)M = V(w). It is equivalent to halting of Neary’s tag systems (M₃(5)).

Tile and role#

A tile is one word pair of a correspondence instance, and a tile word is a sequence of tiles. The four tiles of fixed-boundary correspondence are the rule tiles R_x and the deletion tiles D_x for x ∈ {b, c}; the same symbols denote their matrices. Their pairs (letter, phase) are called roles.

Tag system#

A machine with a queue of letters, a deletion width β, and a word for each letter. A step reads the first letter, appends its word, and deletes the first β letters; the system halts when fewer than β letters remain. The letters deleted by one step form a stroke. At every time, the strokes followed by the queue equal the initial queue followed by the appended words.

Deletion width#

The number β of letters deleted by each tag step. In this series β ≥ 3.

Appendant#

The word appended when a letter is read. In Neary’s binary tag systems the appendants are b for b and Bb for c.

Neary body#

The word B over b, c in the rule c ↦ Bb. The initial queue is B without its first β − 1 letters, followed by b. Neary’s compiler encodes a program and its input in β and B.

Cyclic tag system#

A tag-like machine that cycles through a fixed list of words and appends the current one only when the letter read is 1. It is an intermediate model in the chain from a universal machine to Neary’s binary tag systems.

Kinds of words#

The series uses several alphabets, and a word always belongs to one of them. A tile word lists tiles; a control word lists the matrices of the paired scalar series; a binary word spells another alphabet in a code; a physical word lists the matrices of the actual mortality instance. Compilers map words of one kind to words of another, and a zero of one need not be a zero of the other word for word.

Linear representations#

Semiring#

A set with an addition and a multiplication satisfying the ring axioms except that additive inverses need not exist; the integers, the rationals, and the natural numbers are examples. Interface compression holds over every commutative semiring, since its proof never subtracts.

Rank profile#

The ranks of the generators of a family. M₃(2) splits by rank profile into strata of different difficulty.

Invariant subspace and quotient#

If every generator maps a subspace K into itself, the generators act on the quotient space. If moreover the boundary row vanishes on K, every coefficient survives the passage to the quotient. The paired scalar series is such a quotient.

Rank-one separator#

A generator S = cr built from a column c and a row r. For every product X, SXS = (rXc)S, so a vanishing coefficient becomes a zero product; the converse must be proved for every product in which S occurs.

Boundary row and column#

A row r and a column c that select the coefficient rX_wc of a product. They encode fixed left and right boundary words.

Word series#

A function from words to scalars, such as the coefficient of a word’s product at fixed boundary data.

Linear representation and realization#

A factorization f(w) = λY_wγ of a word series by a row, matrices for the letters, and a column. Its dimension is the size of the matrices. For a single matrix sequence Γ_n, a realization is a triple (A, U, O) with Γ_n = OAⁿU. An exact representation reproduces every value; one that reproduces only the zeros may be smaller.

Hankel matrix and Hankel rank#

The Hankel matrix of a word series f has rows and columns indexed by words and entries f(xy); that of a matrix sequence is the block matrix [Γ_i+j]. It factors through the space of any representation, so its rank bounds the dimension from below, and for matrix sequences the bound is attained (Ho–Kalman). The bound concerns exact representations only.

Paired scalar series#

The three integer 4 × 4 matrices G_b, G_c, T and the column c. The paired coefficient of a control word z is e₁^TG_zc; it vanishes exactly when the tile word decoded from z solves fixed-boundary correspondence.

Phase and toggle#

The paired scalar series stores whether the next data letter selects a rule tile or a deletion tile: the rule phase or the deletion phase. The toggle T switches the phase, and a data letter leaves the deletion phase. In the column G_zc the lower word’s length appears in coordinate two in rule phase and in coordinate four in deletion phase.

Zero set#

The set of words at which a word series vanishes. A reduction to mortality needs only this set, or only whether it is nonempty, not the other values.

Pointwise zero preservation#

Two word series preserve zeros pointwise when they vanish on the same words, possibly after a fixed renaming of words. The tilted separator of M₉(2) does this.

Existential zero transport#

Preserving only whether a nonempty zero word exists, while a witness may be replaced by a different word. The asymmetric separator of M₈(2) rejects some zeros of the paired series and recovers each by prepending a toggle.

Tilted code#

F_s(x) = σ(x) + s·3^|x|. For s < −3/2 it is injective on binary words, because the words of each length fill an interval and these intervals are disjoint (M₈(2)).

Asymmetric separator#

The separator row (1, a, q, q) of M₈(2). Its value is F_q(X) − F_q(Y) in deletion phase and F_q(X) − F_a(Y), never zero, in rule phase.

Ternary value#

For a binary word x, σ(x) is the base-three value of x with the digits 0, 1 replaced by 1, 2; the empty word has value 0. For example σ(01) = 5. Because no digit is 0, σ is injective, and σ(xy) = σ(x)3^|y| + σ(y).

Periodic ternary value#

For a nonempty word w, the value σ(w)/(3^|w| − 1) of the ternary fraction that repeats the recoded digits of w. Two words have the same periodic value exactly when they commute.

Word commutation#

Words u, v commute when uv = vu, equivalently when both are powers of one word. For example 01 and 0101 commute.

Word-pair matrices#

The 3 × 3 matrices Ψ(x, y) with Ψ(xx′, yy′) = Ψ(x, y)Ψ(x′, y′), whose upper-right entry σ(x) − σ(y) vanishes exactly when x = y. Conjugating by a unimodular matrix gives Φ(u, v), in which the two words occupy separate coordinates.

Agreement plane#

The plane E = span{e₁, e₃} on which the rule and deletion matrices of one letter agree, because they have the same upper word. The paired scalar series and the binary compilers share it between decoder states.

Compilers and return systems#

Compiler#

An explicit map from instances of one problem to instances of another, with a forward theorem and a converse that covers every word of the target instance. It is a reduction once the map is computable.

Paired-role compression#

The quotient construction that replaces four maps agreeing in pairs on an r-dimensional subspace by two data maps and a toggle in dimension 2d − r.

Binary compiler#

A compiler that replaces a larger alphabet by two generators, spelling letters in a binary code and storing an unfinished codeword in the matrix blocks. Its converse must cover complete codewords, unfinished suffixes, and words that start in any decoder state.

Common-image restriction#

Restricting a family whose generators all map into one subspace to that subspace. Restriction can create zero products; in the binary compilers one appended letter turns each of them into a zero product of the original family.

Transition#

A generator designated to occur between cuts. With one transition A, the number of consecutive transitions between two cuts is the wait n.

Cut#

A generator designated to factor through a smaller space, C = UO. Every product containing it passes through that space. “Transition” and “cut” name roles in an analysis of an ordinary family; they add no matrices and restrict no words.

Factored cut#

A cut presented as C_j = U_jO_j, with O_j mapping into an interface space and U_j mapping back. The factorization need not be of minimal rank.

Interface space#

The space through which a cut factors. Its dimension may exceed the rank of the cut.

Interface bridge#

For cuts i, j and a transition word w, the map O_iA_wU_j of the interface. Consecutive cuts in a product contribute consecutive bridges of a path.

Interface compression#

The theorem that a family of transitions and factored cuts is mortal exactly when the transitions alone are mortal or some path of interface bridges has zero product.

Physical family#

The finite family of matrices given to the mortality problem, as opposed to an infinite family of returns or an intermediate alphabet. A physical word is any nonempty word over it.

Return#

For one transition A and one cut UO, the return after wait n is Γ_n = OAⁿU. A physical word with several cuts corresponds to a product of returns, one for each run of transitions between cuts.

Singular-return compression#

The theorem that {A, UO} is mortal exactly when its returns are, provided no power of A vanishes. Neither the cut nor U, O need be invertible.

Return realization#

A triple (A, U, O) whose returns are a prescribed sequence, for instance the three paired controls followed by multiples of a separator. Its least dimension is the Hankel rank of the sequence.

Exterior wait and pure transition word#

Transitions before the first cut or after the last are exterior waits; a word with no cut is a pure transition word. A converse for unrestricted products must handle both.

Tail and residuals#

When the returns from time three on are ξ²⁻ⁿS, extending this geometric tail back to times 0, 1, 2 and subtracting it leaves residuals N₀, N₁, N₂. An invertible part of the transition realizes the tail and a nilpotent part the residuals.

Nilpotent chains and eigenline#

A nilpotent Jordan chain of length ℓ contributes to returns at times 0, …, ℓ − 1 only; an eigenline with nonzero eigenvalue carries a geometric tail and keeps every power of the transition nonzero. For residuals supported on times 0, 1, 2, the least number of chains of length three is rank N₂, and those of lengths two and one supply what the longer chains cannot.

Denominator clearing#

Multiplying each rational generator by its own nonzero integer. Every product is multiplied by a nonzero scalar, so zero products are preserved and reflected. For a computable reduction the entries are evaluated as unreduced fractions, which keeps the map primitive recursive.

Arithmetic dynamics#

Projective line#

The nonzero columns (x, y)^T up to a common nonzero factor, with affine coordinate x/y and the point at infinity y = 0. An invertible 2 × 2 matrix acts on it by a Möbius map z ↦ (az + b)/(cz + d), and a nonzero row defines the point of its kernel.

Projective incidence#

Whether some product of given invertible 2 × 2 matrices moves a given column into the kernel of a given row: ∃w r^TX_wc = 0. GPI₂ is the two-generator restriction normalized so that two chart scalars equal 1.

Shortcut Collatz map#

The map x ↦ x/2 for even x and x ↦ (3x + 1)/2 for odd x. Reachability asks, for one given integer, whether some iterate is 1; the Collatz conjecture asserts this for every positive integer.

p-adic valuation#

For a prime p and a nonzero rational x, v_p(x) is the exponent of p in x, negative for denominators. It satisfies v_p(x + y) = min(v_p(x), v_p(y)) whenever the two valuations differ, so terms of different valuation cannot cancel.

p-adic unit#

A nonzero rational of p-adic valuation zero.

Live region and trap#

In the valuation guard, the live points are the nonzero rationals of positive p-adic valuation. The trap is a set that every return maps into itself and that excludes the target 1; a point that enters it can never reach 1 (valuation guard).

Valuation guard#

A family of pairs in M₃(2) whose returns admit, at each live point, only the wait equal to the point’s p-adic valuation, so that mortality becomes reachability of 1 along one deterministic orbit.

Ready point and legal wait#

In the valuation guard, the legal wait at a live point is its p-adic valuation. The point is ready if it also satisfies the carry-depth condition under which that wait avoids the trap. A ready orbit may still continue forever.

Reset, target, and tail#

The reset is the point ρ to which the separator sends every orbit; the target is the point 1 that the separator tests for. The tail coordinate of a ready point is the unit X in its normal form p^a + p^sa/X.

Valuation wall#

A ball in a p-adic or ℓ-adic metric that contains the reset, is preserved by every legal step, and excludes the target. Its existence proves the corresponding pair immortal.

Reset-defect numerator#

For α = N/L and δ = D/L with integers N, D, L, the integer R = N + D − L = L(ρ − 1), the distance from reset to target after clearing denominators.

Primitive pair and content#

A pair of coprime integers representing a point of the projective line. The content is the common factor, possibly signed, removed to reach it.

Smith split#

In the valuation guard at depth two, a factorization of the content removed by one legal step, and of its complementary factor, into factors fixed by the parameters and factors depending on the wait.

Exact-order prime and primitive divisor#

A prime ℓ has exact order n for the base p if pⁿ ≡ 1 modulo ℓ and no smaller positive exponent works. A primitive divisor of pⁿ − 1 is a prime of exact order n.

Verification and evidence#

Machine-checked theorem#

A theorem whose Lean proof passes this repository’s strict build. It establishes the formal statement; whether that statement matches the prose is a separate question, answered by the formal-scope notes.

Transitive axiom set#

The axioms a theorem depends on after following every declaration it uses. This project compares the complete set for each publication-facing theorem with a reviewed snapshot and admits only propext, Classical.choice, and Quot.sound.

Trust boundary#

What must be trusted rather than proved: the Lean kernel, the pinned libraries, and the fidelity of the definitions to the problems they name.

Formal scope#

The boundary between claims proved in Lean and claims supported only by prose, audit, or computation. Each page states it in its Bookkeeping section.

Symbolic cross-check#

An independent exact computation, usually in a computer algebra system, that reconstructs identities already proved in Lean. It is not a premise of any theorem.

Finite falsifier#

A bounded exhaustive search for counterexamples to a universal claim. It excludes counterexamples only within its bound and is not a proof.

Obstruction#

A proved limit of a stated construction or family, such as a lower bound on the dimension of its realizations. It does not bound the underlying problem unless it quantifies over all constructions.

Sources#

Mortality and reduction terminology follows Cassaigne, Halava, Harju, and Nicolas; GPCP terminology follows Nicolas; tag-system vocabulary follows Neary; realization and Hankel rank follow linear systems theory and weighted-automata theory. Terms introduced by this series are defined in the linked articles.

1. Julien Cassaigne, Vesa Halava, Tero Harju, and François Nicolas, Tighter Undecidability Bounds for Matrix Mortality, Zero-in-the-Corner Problems, and More, 2014.
2. François Nicolas, (Generalized) Post Correspondence Problem and Semi-Thue Systems, 2008.
3. Turlough Neary, Undecidability in Binary Tag Systems and the Post Correspondence Problem for Five Pairs of Words, STACS 2015.
4. B. L. Ho and R. E. Kalman, Effective Construction of Linear State-Variable Models from Input/Output Functions, Regelungstechnik 14, 1966.
5. Stefan Kiefer, Notes on Equivalence and Minimization of Weighted Automata, 2020.
6. Formal Verification, theorem map and trust boundary for this series.