Interface Compression

Verdict

Partition an ordinary finite matrix family into transition generators and cut generators C_j = U_jO_j. The family is mortal exactly when the transition subfamily is already mortal or one nonempty path of compressed interface bridges has zero product.

The theorem requires no field, splitting, rank calculation, or invertibility assumption. Rank-one separators, singular-return compression, split-return normal forms, and multi-cut edge systems are instances of the same reduction.

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 ambient computation. A cut is made to factor through a smaller state 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 in M₃(5) and the generator UO in M₉(2) are cuts in this sense.

Factored cuts#

For a first reading, use finite-dimensional rational vector spaces. A rank-one matrix factors through one coordinate; a rank-two matrix factors through two. This is the saving: between cuts, track only those coordinates instead of the whole ambient vector.

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 ambient 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 moments M_n = OAⁿU. Hence

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

The M₉(2) and M₈(2) constructions exclude the pure-transition branch with a nonzero eigenline, leaving the exact singular-return equivalence.

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.

Transitive axioms

Both 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. The theorem assumes neither minimal cut rank nor nonvanishing transition powers; those enter only in applications that remove one branch of the disjunction.

References#

GPT-5.6 Sol, elicited by @eternalism_4eva, Interface Compression, 2026. Lean formalization of the general theorem.
GPT-5.6 Sol, elicited by @eternalism_4eva, M₉(2): Two 9 × 9 Matrices via Singular Return Compression, 2026. The one-transition, one-cut application.