Interface Compression

Split a finite matrix family into transition generators and cut generators, each cut factored as C_j = U_jO_j through a smaller interface space. The family is mortal exactly when the transitions alone are mortal or some path of interface bridges O_iA_wU_j has zero product. Mortality of a large family thereby reduces to mortality of small matrices.

The theorem holds over every commutative semiring and assumes no rank, invertibility, or minimality. Rank-one separators, the returns of a single transition and a single cut, and systems with several cuts are instances. For one transition A and one cut UO with no vanishing power of A, mortality of the pair equals mortality of the returns OAⁿU, and a return family with finitely many shapes up to scaling reduces to a finite family.

Known Stuff#

From generators to cuts#

Begin with an ordinary mortality instance: one finite labelled family of matrices. Partition its labels into transition labels α and cut labels J, and write

G = {A_{a} : a \in α} ⨿ {C_{j} : j \in J} .

No matrix is added and no word grammar is imposed: mortality still quantifies over every nonempty word in the original family. “Transition” and “cut” name roles in the analysis.

In a reduction, transitions carry the computation. A cut is made to factor through a smaller space, so every word containing it must pass through a controlled interface. The theorem separates transition-only words from cut-containing words and compresses the latter. The rank-one separator of M₃(5) and the second generator UO of M₉(2) and M₈(2) are cuts in this sense.

Factored cuts#

For a first reading, take finite-dimensional rational vector spaces. A rank-one matrix factors through a line and a rank-two matrix through a plane. Between two cuts, a product then needs to track only a vector of the interface, not a vector of the whole space.

Let L be the physical state space and S an interface space. A factored cut has the form

C_{j} = U_{j} O_{j}, U_{j} : S \to L, O_{j} : L \to S .

The map O_j sends the physical state to the interface; U_j returns it to L. Thus an occurrence of C_j forces the product through S at that position. Every matrix has a trivial factorization through L; the construction becomes a compression when S is smaller. No minimal factorization is required.

Physical words#

A physical word is a word in the original generator labels. Write A_w for the ordered product of a transition word, with the empty word giving the identity. Every physical word is either transition-only or has a unique block form

A_{u_{0}} C_{j_{1}} A_{u_{1}} \dots C_{j_{q}} A_{u_{q}}, q \geq 1,

where each transition block u_t may be empty. Between two cuts, associativity exposes

C_{i} A_{w} C_{j} = U_{i} (O_{i} A_{w} U_{j}) O_{j} .

The parenthesized matrix is the interface bridge between cut i on the left and cut j on the right:

B_{i, w, j} = O_{i} A_{w} U_{j} : S \to S .

The exterior blocks u₀ and u_q are not discarded. If the displayed physical word is zero, sandwiching it by O_j₁ and U_{j_q} gives

(O_{j_{1}} A_{u_{0}} U_{j_{1}}) (O_{j_{1}} A_{u_{1}} U_{j_{2}}) \dots (O_{j_{q}} A_{u_{q}} U_{j_{q}}) = 0 .

The first and last factors are endpoint loops carrying the leading and trailing transition blocks. This is the compressed path promised by the theorem.

New Stuff#

General theorem#

Interface compression. Over any commutative semiring, with finite coordinate spaces L and S, the family of transitions and factored cuts is mortal if and only if either the transitions alone are mortal or there are cuts j₀, …, j_r and transition words w₁, …, w_r, with r ≥ 1, such that

\prod_{t = 1}^{r} O_{j_{t - 1}} A_{w_{t}} U_{j_{t}} = 0 .

Proof#

A cut-free zero word is already a zero transition word. For a cut-containing zero, the sandwich calculation above gives a nonempty zero path of interface bridges. Its endpoint loops retain the leading and trailing transition blocks.

Conversely, spell a bridge path as a physical word beginning with its first cut. Associativity gives

C_{j_{0}} A_{w_{1}} C_{j_{1}} \dots A_{w_{r}} C_{j_{r}} = U_{j_{0}} (bridge-path product) O_{j_{r}} .

A zero bridge path therefore gives an actual nonempty zero word in the original generators.

Rank-one interfaces#

When S is one-dimensional, write each cut as c_jr_j^T. Every bridge is the scalar

r_{i}^{T} A_{w} c_{j} .

Over a field, a product of one-dimensional bridges vanishes exactly when one scalar factor vanishes. Apart from the transition-only branch, mortality therefore reduces to one row–word–column incidence. The repeated rank-one separator is the one-cut instance; its nonsingular transitions exclude the other branch.

Single-cut return families#

With one cut C = UO, the bridge alphabet is the complete return family

{O A_{w} U : w \in α^{*}} .

If there is one transition A, these are the returns

Γ_{n} = O A^{n} U, n \geq 0,

where n is the number of transitions between two cuts. The theorem becomes

Mortal {A, UO} \Leftrightarrow (\exists n \geq 1 : A^{n} = 0) \lor Mortal {Γ_{n} : n \geq 0} .

When no power of A vanishes, for instance when A is invertible or has a nonzero eigenvalue, the first branch is empty and two physical matrices present the infinite family {Γ_n}. This is singular-return compression: neither the cut nor the maps U, O need be invertible or of full rank. Both directions are explicit:

\begin{array}{l} A^{p_{0}} C A^{p_{1}} C \dots C A^{p_{r}} = 0 \Rightarrow Γ_{p_{0}} Γ_{p_{1}} \dots Γ_{p_{r}} = 0, \\ C A^{p_{0}} C \dots A^{p_{r}} C = U (Γ_{p_{0}} \dots Γ_{p_{r}}) O . \end{array}

The first line multiplies a zero physical word by O on the left and U on the right, so the transitions before the first cut and after the last cut become the first and last returns. The second wraps a return product in cuts.

Finitely many return shapes#

Suppose that over a field every return is a nonzero multiple of one of finitely many matrices F₁, …, F_m, say Γ_n = ρ_nF_ℓ(n) with ρ_n ≠ 0, and that every F_i occurs. Then {Γ_n} and {F₁, …, F_m} are mortal together: a product of returns is a nonzero scalar times the corresponding product of the F_i, and every word in the F_i lifts to a word in returns by choosing, for each i, one n with ℓ(n) = i. A design that prescribes the returns at finitely many times and makes every later return a multiple of one fixed matrix therefore presents a finite family with two physical matrices.

Many cuts#

Several cuts form a directed graph. Vertices are cut labels, and the edge from i to j carries $O_{i} A_{w} U_{j}$ . Edge order follows the written matrix word; its action on column vectors runs in the opposite direction. Successive edges must share a cut label, because they come from adjacent blocks of one word. This is why the theorem asks for a zero path, not an arbitrary product of unrelated bridges. Transition-only zeros remain a separate branch.

Bookkeeping#

Verification and provenance#

General compression

InterfaceCompression.isMortal_iff proves the transition-or-path equivalence over an arbitrary commutative semiring.

Rank-one specialization

InterfaceCompression.isMortal_rankOne_iff retains the transition-only alternative and reduces the cut-containing branch to one scalar bridge incidence.

Singular-return compression

pairGenerator_isMortal_iff_returnFamily proves that {A, UO} and its return family are mortal together when no power of A vanishes.

Transitive axioms

These declarations use only propext, Classical.choice, and Quot.sound.

Formal scope#

The physical spelling, arbitrary-word block decomposition, exterior-block sandwich, bridge-path converse, general theorem, and rank-one scalar specialization are machine-checked, as is singular-return compression. The theorem assumes neither minimal cut rank nor nonvanishing transition powers; those enter only in applications that remove one branch of the disjunction. The lemma on finitely many return shapes has no generic Lean declaration; its instances in M₉(2) and M₈(2) are machine-checked.

References#

GPT-5.6 Sol, elicited by @eternalism_4eva, M₈(2): Mortality of Two 8 × 8 Integer Matrices, 2026. Two applications with one transition and one cut, in dimensions nine and eight.
GPT-5.6 Sol, elicited by @eternalism_4eva, Shortcut-Collatz Incidence, 2026. An application to two-generator projective incidence.