Binary Compilers

Known Stuff#

Four-role source#

The fixed-boundary correspondence theorem supplies four roles R_x, D_x, with x ∈ {b, c}, and a terminal column c. A role word w satisfies the fixed-boundary equation exactly when

e_{1}^{T} X_{w} c = 0 .

The source problem is undecidable. The four matrices are nonsingular; adjoining the rank-one boundary matrix gives the five-matrix family used for M₃(5).

Shared channel#

The side-normal basis writes every word-pair matrix as

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

For each fixed source letter x, the rule and deletion roles have the same upper word u_x. They therefore agree on the upper plane

E = span {e_{1}, e_{3}}, R_{x} | E = D_{x} | E .

Paired-role compression identifies this plane between two phases. The compilers below instead share it between partial binary decoder states.

Previous binary bounds#

Cassaigne, Halava, Harju, and Nicolas established Z₉(2), R₁₀(2), and M₁₅(2), together with general alphabet-packing and scalar-to-corner reductions [Cassaigne et al. 2014]. The fixed-boundary result and their mortality packing give M₁₂(2). Binary codes and incomplete-codeword decoders are prior techniques; the constructions below use the paired source identity to remove states from the corresponding generic realizations.

New Stuff#

Results#

The source alphabet factors as a phase bit R/D and a letter bit b/c. The scalar compiler stores one shared unfinished upper channel and preserves every coefficient in six states. The mortality compiler represents all five source matrices by a complete prefix decoder, then restricts its common image from twelve states to ten.

Six-state scalar compiler#

Two-bit code#

Every binary pair denotes one role:

\begin{array}{rcl} 00 & \mapsto & R_{b}, \\ 01 & \mapsto & R_{c}, \\ 10 & \mapsto & D_{b}, \\ 11 & \mapsto & D_{c} . \end{array}

Write U_x = σ(u_x), A_x = 3^|u_x|, V_x^p = σ(v_x^p), and B_x^p = 3^{|v_x^p|}.

Generators#

Use row coordinates (a, λ, υ, λ_R, υ_*, λ_D). The two integer matrices are

N_{0} = (\begin{matrix} 1 & 0 & 0 & 0 & 0 & 0 \\ 0 & 0 & 0 & 1 & 0 & 0 \\ 0 & 0 & 0 & 0 & 1 & 0 \\ V_{b}^{R} & B_{b}^{R} & 0 & 0 & 0 & 0 \\ U_{b} & 0 & A_{b} & 0 & 0 & 0 \\ V_{b}^{D} & B_{b}^{D} & 0 & 0 & 0 & 0 \end{matrix}),

N_{1} = (\begin{matrix} 1 & 0 & 0 & 0 & 0 & 0 \\ 0 & 0 & 0 & 0 & 0 & 1 \\ 0 & 0 & 0 & 0 & 1 & 0 \\ V_{c}^{R} & B_{c}^{R} & 0 & 0 & 0 & 0 \\ U_{c} & 0 & A_{c} & 0 & 0 & 0 \\ V_{c}^{D} & B_{c}^{D} & 0 & 0 & 0 & 0 \end{matrix}) .

The first three coordinates form the root state. The remaining coordinates store the unfinished lower rule channel, one upper channel shared by both phases, and the unfinished lower deletion channel.

Arbitrary binary words#

For a row triple q = (a, λ, υ), put

\begin{array}{rcl} E (q) & = & (a, λ, υ, 0, 0, 0), \\ O_{R} (q) & = & (a, 0, 0, λ, υ, 0), \\ O_{D} (q) & = & (a, 0, 0, 0, υ, λ) . \end{array}

Direct multiplication gives

\begin{array}{ll} E (q) N_{0} = O_{R} (q), & E (q) N_{1} = O_{D} (q); \\ O_{R} (q) N_{x} = E (q X_{R, x}^{T}), & O_{D} (q) N_{x} = E (q X_{D, x}^{T}) . \end{array}

Parse a binary word from the left into complete pairs and discard one final bit when the length is odd. If the pairs decode as a₁, …, a_n, define τ(z) = a_n⋯a₁. The reversal accounts for the transposed row action. With

L_{6} = (μ, - 1, t, 0, 0, 0), C_{6} = e_{1},

the transition identities give, for every binary word,

L_{6} N_{z} C_{6} = e_{1}^{T} X_{τ (z)} c .

An unpaired final bit changes only the unfinished phase and preserves the extracted first coordinate. Conversely, encoding the reversed sequence of any role word gives a binary preimage. The decoder is total and surjective.

Structured form#

Transposing both generators makes their first column e₁. Product reversal is a bijection on binary words, so scalar zero reachability is unchanged. The empty and one-bit coefficients equal μ ≠ 0; the free-monoid and nonempty free-semigroup conventions therefore agree. This proves structured Z̊₆(2), hence Z₆(2). The standard integral scalar-to-corner lift gives R₇(2) [Cassaigne et al. 2014].

Ten-state mortality compiler#

Complete prefix code#

Transpose the normalized five-matrix family and write its rank-one separator as Π = e₁c^T. Denote the four payloads by R_c, R_b, D_c, D_b. For every p in the upper plane E,

p^{T} R_{x} = p^{T} D_{x} .

Use the complete prefix code

\begin{array}{rcl} 0 & \mapsto & Π, \\ 100 & \mapsto & R_{c}, \\ 101 & \mapsto & R_{b}, \\ 110 & \mapsto & D_{c}, \\ 111 & \mapsto & D_{b} . \end{array}

Its proper-prefix states are ε, 1, 10, and 11.

Twelve-state realization#

Order four three-dimensional blocks by those prefix states. The binary generators are

𝒜_{0} = (\begin{matrix} Π & 0 & 0 & 0 \\ 0 & 0 & I & 0 \\ R_{c} & 0 & 0 & 0 \\ D_{c} & 0 & 0 & 0 \end{matrix}), 𝒜_{1} = (\begin{matrix} 0 & I & 0 & 0 \\ 0 & 0 & 0 & I \\ R_{b} & 0 & 0 & 0 \\ D_{b} & 0 & 0 & 0 \end{matrix}) .

Each block row contains one nonzero block. For every start state and binary word, its product therefore has one possibly nonzero block in that row: the deterministic final prefix state selects the column, and the emitted source product is the block value. This covers complete codewords, unfinished suffixes, and every starting prefix state.

Synchronizer#

The word 00 sends every prefix state to ε. Its four emitted products are

\begin{aligned} ε : & Π^{2}, \\ 1 : & R_{c}, \\ 10 : & R_{c} Π, \\ 11 : & D_{c} Π . \end{aligned}

If a source word w has zero matrix product, then 00 followed by its prefix encoding makes every block row zero. Conversely, a zero binary product has a zero root block, whose emitted source product cannot be empty because the empty product is the identity. Thus the twelve-state pair is mortal exactly when the five-matrix source family is mortal.

Common-image restriction#

For p ∈ E, define the row ℓ_p = (0, 0, p^T, −p^T) in the four prefix blocks. Paired-role agreement gives

ℓ_{p} 𝒜_{0} = ℓ_{p} 𝒜_{1} = 0 .

The independent choices p = e₁, e₃ place both images in the ten-dimensional subspace

K = \ker ℓ_{e_{1}} \cap \ker ℓ_{e_{3}} .

A vector in K has block coordinates

(x_{1}, x_{2}, x_{3} | y_{1}, y_{2}, y_{3} | a, b, c | a, d, c) .

Let J embed the ten displayed coordinates into this vector, and let Q extract them, so QJ = I₁₀. Define

B_{i} = Q 𝒜_{i} J (i \in {0, 1}) .

The coordinates are integral. Since each image lies in K,

𝒜_{i} J = J B_{i} .

Mortality converse#

If a twelve-state product 𝒜_z is zero, then B_z = Q𝒜_zJ = 0. Conversely, if B_z = 0, then 𝒜_z kills K. Because the image of 𝒜₀ lies in K,

𝒜_{z} 𝒜_{0} = 𝒜_{z 0} = 0 .

The appended letter converts every zero introduced by restriction into a zero of the twelve-state decoder, which in turn yields a nonempty zero source product. Hence the two 10 × 10 integer matrices are mortal exactly when the fixed-boundary source halts.

Consequences#

The six-state construction changes the two-generator scalar and corner bounds to Z₆(2) and R₇(2). The ten-state construction changes the two-generator mortality bound to M₁₀(2). For every n ≥ 0,

B_{i} \mapsto B_{i} \oplus 0_{n}

preserves zero products, proving M_10+n(2). The series landing page records the resulting current frontiers.

Bookkeeping#

Verification and provenance#

Six-state compiler

Lean checks the explicit generators, every binary word, odd residues, coefficient preservation, decoder surjectivity, and common-first-column transport.

Prefix transducer

Lean proves the arbitrary-word block-row theorem used by the complete prefix decoder.

Ten-state compiler

Lean checks synchronization, twelve-state mortality, the common image, integral restriction, the appended-letter converse, and zero padding.

Transitive axioms

Publication-facing declarations use only propext, Classical.choice, and Quot.sound. The project contains no admitted proof or project axiom.

Formal scope#

Lean proves the complete instance-level equivalences. The canonical declarations are nearyScalarZero62_hasZero_iff_tagHaltsFrom, nearyScalarZero62_hasZeroStar_iff_tagHaltsFrom, nearyMortality102_mortal_iff_tagHaltsFrom, and nearyMortality10Plus_mortal_iff_tagHaltsFrom.

The computable reduction from mathlib’s code-halting predicate to the restricted binary-tag source is machine-checked; Neary’s construction is provenance rather than an imported theorem [Neary 2015]. The six- and ten-state target equivalences are machine-checked. Primitive-recursive declarations for those target constructors and their final many-one wrappers remain formalization debt. Frontier transports and priority claims are external to Lean.

Priority#

To our knowledge, after public-literature searches through 24 July 2026, no prior proof establishes Z₆(2), R₇(2), or M₁₀(2). CHHN’s corresponding established bounds are Z₉(2), R₁₀(2), and M₁₅(2) [Cassaigne et al. 2014]. Prefix coding, alphabet reduction, and scalar-to-corner transport are prior art. No source was found for the shared six-state partial channel or the ten-dimensional common-image restriction and its appended-letter mortality converse. “No prior proof found” is limited to publicly discoverable work.

References#

GPT-5.6 Sol, elicited by @eternalism_4eva, Fixed-Boundary Correspondence, 2026. The four-role source and five-matrix compiler.
GPT-5.6 Sol, elicited by @eternalism_4eva, Paired-Role Compression, 2026. The shared side-normal channel and four-dimensional quotient.
Turlough Neary, Undecidability in Binary Tag Systems and the Post Correspondence Problem for Five Pairs of Words, STACS 2015. The restricted binary-tag undecidability 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. Prior bounds and standard transports.
Günter Rote, Probabilistic Finite Automaton Emptiness Is Undecidable for a Fixed Automaton, MFCS 2025. Related binary prefix decoding with explicit treatment of unfinished codewords.