The Valuation Guard

Known Stuff#

The frontier cell#

M₃(2) asks whether some nonempty word in two supplied 3 × 3 integer matrices equals zero. It is the first unresolved cell in the three-dimensional, two-generator corner of the bounded mortality table.

If both matrices are invertible, every product is invertible. The first difficult rank profile therefore has one invertible generator and one generator of rank two. Write them as A and B.

Return compression#

A split rank-two cut#

Over ℚ, factor the rank-two matrix through a two-dimensional interface:

B = U V, U : ℚ^{2} \to ℚ^{3}, V : ℚ^{3} \to ℚ^{2} .

A block beginning and ending with B then collapses to the interface. Define the return after n ambient steps by

G_{n} = V A^{n} U \in M_{2} (ℚ) .

Return products#

For any waits n₁, …, n_k,

B A^{n_{1}} B A^{n_{2}} B \dots A^{n_{k}} B = U G_{n_{1}} G_{n_{2}} \dots G_{n_{k}} V .

Because A is invertible and U, V have full interface rank, exterior powers of A cannot create or hide a zero. Mortality of the physical pair is therefore exactly mortality of the infinite return family. This is the split-return normal form.

The problem is not an ordinary scalar recurrence. A word may choose a different unbounded index n at every return, producing a product of recurrence values. Linear recurrence automata provide nearby vocabulary for this controlled setting [Hirvensalo et al. 2024].

Two arithmetic languages#

The projective line#

A nonzero column (x,y)^T determines the projective point z = x/y. Columns differing by a nonzero scalar represent the same point; y = 0 represents infinity. An invertible 2 × 2 matrix acts by a Möbius transformation.

Projectivization forgets scale but preserves exactly the information needed by a rank-one separator. If the separator’s terminal row is (1,−1), it kills precisely the projective point z = 1.

The p-adic valuation#

Fix a prime p. For a nonzero rational number, v_p records the exponent of p in its reduced factorization. Thus

v_{p} (p^{3} \cdot \frac{7}{11}) = 3 .

A rational is a p-adic unit when its valuation is zero. The ultrametric law makes unequal valuations rigid:

v_{p} (x) \neq v_{p} (y) \Rightarrow v_{p} (x - y) = \min (v_{p} (x), v_{p} (y)) .

The guard uses this law to compare an arbitrarily selected wait against an unbounded integer stored in the current projective point.

New Stuff#

Result#

Amalgamated valuation guard. Fix a prime p, a depth s ≥ 2, a center α, and a reset ρ. Assume α and α−1 are p-adic units and ρ has positive valuation. The two rational 3 × 3 matrices constructed below are mortal exactly when the deterministic guarded orbit starting at ρ reaches 1.

The result does not decide that reachability problem. It removes the matrix-semigroup freedom surrounding it: separator placement, arbitrary words, incorrect waits, affine poles, and infinity are all covered by the equivalence.

The three-mode family#

Ambient action and cut#

Put δ = ρ−α. The hypotheses imply that δ is also a p-adic unit. Take

A = [\begin{matrix} 1 & 0 & 0 \\ 0 & p^{- 1} & 0 \\ 0 & 0 & p^{s - 1} \end{matrix}], U = [\begin{matrix} 0 & 1 \\ 1 & 0 \\ 1 & - 1 \end{matrix}],

V = [\begin{matrix} - α & α & δ \\ - 1 & 1 & 0 \end{matrix}], B = U V = [\begin{matrix} - 1 & 1 & 0 \\ - α & α & δ \\ 1 - α & α - 1 & δ \end{matrix}] .

The ambient matrix has three distinct arithmetic modes: constant, contracting by p, and expanding by p^s−1. The cut B has rank exactly two.

Return matrices#

The return G_n = VAⁿU is

G_{n} = [\begin{matrix} α p^{- n} + δ p^{(s - 1) n} & - α - δ p^{(s - 1) n} \\ p^{- n} & - 1 \end{matrix}] .

At zero wait,

G_{0} = [\begin{matrix} ρ \\ 1 \end{matrix}] [\begin{matrix} 1 & - 1 \end{matrix}], G_{0}^{2} = (ρ - 1) G_{0} .

It is a nonnilpotent rank-one separator: it resets every non-kernel projective point to ρ and tests whether the incoming point is 1. Every positive return is invertible because

\det (G_{n}) = δ p^{(s - 2) n} (1 - p^{n}) \neq 0 (n \geq 1) .

The physical separator is already the word B² = UG₀V. No third generator is added.

The projective guard#

The defect identity#

Multiplying G_n by the nonzero scalar pⁿ does not change its projective action. In affine coordinate z, the resulting map is

Φ_{n} (z) = \frac{(α + δ p^{s n}) z - α p^{n} - δ p^{s n}}{z - p^{n}} .

Its numerator and denominator satisfy the cross-multiplied identity

Φ_{n} (z) - α = δ p^{s n} \frac{z - 1}{z - p^{n}} .

This identity compares the current valuation, the chosen wait, and the terminal defect z−1. The formal proof uses the cross-multiplied form, so the pole z = pⁿ is not silently discarded.

The permanent trap#

The live region consists of finite nonzero points of positive p-adic valuation. The target 1 is admitted separately. Define

Live = {z \in ℚ : v_{p} (z) > 0}, Trap = ℙ^{1} (ℚ) ∖ (Live \cup {1}) .

For every positive wait, the trap maps into itself. Negative-valuation points, zero, infinity, and nonterminal units all enter the unit residue ball around α. Since α−1 is a unit, that ball excludes the target 1. The same argument applies again at every later step.

Forced computation#

Wrong waits#

Suppose the current point is live and put a = v_p(z) > 0. Then z−1 is a unit. If the word chooses n ≠ a, unequal valuations give

v_{p} (z - p^{n}) = \min (a, n) .

The defect identity then yields

v_{p} (Φ_{n} (z) - α) = s n - \min (a, n) > 0 .

The output is therefore a nonterminal unit in the trap. Every successful physical word must choose the unique wait

n = v_{p} (z) .

Carry depth#

The correct wait survives only when the state has the required p-adic precision. Write z = p^au, where u is a unit, and put h = v_p(u−1). For u ≠ 1,

v_{p} (Φ_{a} (z) - α) = (s - 1) a - h .

If the right side is positive, the output is a trapped unit; if negative, the output has negative valuation; if z = p^a, the output is infinity. Survival forces the exact ready condition

v_{p} (z) = a, v_{p} (z - p^{a}) = s a .

The tail recurrence#

Ready coordinates#

Every ready point has a unique p-adic unit tail X:

E (a, X) = p^{a} + \frac{p^{s a}}{X}, v_{p} (X) = 0 .

The visible valuation a selects the only legal wait. The tail X carries the remaining unbounded information. Substitution into the legal return gives the deterministic update

Φ_{a} (E (a, X)) = α + δ (p^{s a} + (p^{a} - 1) X) .

The next valuation and next tail are recovered from this rational output. Failure of the next ready condition enters the trap.

Inverse grammar#

The local transition graph is not impoverished. Given positive valuations a, b and any unit target tail X′, define

I_{a, b} (X') = \frac{p^{b} + p^{s b} / X' - α - δ p^{s a}}{δ (p^{a} - 1)} .

This predecessor tail is always a unit and satisfies

Φ_{a} (E (a, I_{a, b} (X'))) = E (b, X') .

Every ready valuation cylinder can therefore reach every other. This is local symbolic completeness, not universality: one initial rational tail must satisfy the entire itinerary.

Arbitrary physical words#

The free semigroup may place A and B in any order. The proof first fractures a zero product at occurrences of the internal separator B². Positive returns between separators act on projective states from right to left, matching matrix multiplication on columns.

Trap invariance propagates through every suffix of a successful bridge. A suffix cannot reach 1 early, because another positive return sends 1 into the trap. Every intermediate state is therefore live, and the forcing theorem makes its selected wait equal its valuation and its carry depth exact. Thus every successful arbitrary word is a legal path.

Conversely, every legal path is represented by its sequence of positive waits. The resulting equivalence is

\begin{array}{c} the physical pair {A,B} is mortal \\ \Leftrightarrow \\ some positive-return projective orbit sends ρ to 1 \\ \Leftrightarrow \\ the functional legal-step relation reaches 1 from ρ. \end{array}

The coefficient Hankel section of the return series has rank three. The construction cannot be reproduced exactly in two linear states.

Concrete pairs#

Take p = 5, s = 2, ρ = 30, and α = 869/28. The reset is ready and its unique legal wait one reaches the target. Clearing denominators gives

A = [\begin{matrix} 5 & 0 & 0 \\ 0 & 1 & 0 \\ 0 & 0 & 25 \end{matrix}], B = [\begin{matrix} - 28 & 28 & 0 \\ - 869 & 869 & - 29 \\ - 841 & 841 & - 29 \end{matrix}] .

B^{2} A B^{2} = 0 .

The guard does not force termination. At p = 5, s = 2, ρ = 5/6, and α = 2, the ready reset is a nonterminal fixed point.

Parity and maximal isolation#

Odd-resultant immortality#

Choose integral coefficients A, D, and L with L ≠ 0 so that α = A/L and the drift δ = D/L. Put

R = A + D - L .

The adjacent unit assumptions on α and α−1 force p to be odd. In primitive terminal-endpoint coordinates, one legal wait a and its removed content h obey

\begin{array}{rcl} p^{s a} h t^{'} & = & r - L (p^{a} - 1) t, \\ h r^{'} & = & D r + (A - L) h t^{'} . \end{array}

If r is odd, the first equation makes h and t′ odd. If R is odd, the second then makes r′ odd. The reset endpoint numerator is R, whereas the canonical physical target has endpoint numerator zero. Induction through the checked decoded-to-primitive lift therefore proves that odd R is a physical immortality certificate.

Maximal steps are isolated#

Only even R remains. At critical depth s = 2, write q = p^a. The forward and complementary contents have the signed Smith split

h = η u, k = θ v, η θ = D L, u v = q - 1 .

The unique noncontracting allocation is v = 1. Its apparent system collapses, after substitution and cancellation, to

r^{'} = θ t + (D q^{2} + A - L) t^{'} .

Here t and θ are odd, while the second coefficient is even. Thus r′ is odd and the maximal step cannot terminate. If another primitive step follows, its Smith coordinate v is even and therefore lies on the v ≥ 2 side. Maximal steps cannot occur consecutively.

The open arithmetic core#

Define a deterministic partial map on rational projective points. At a ready positive-valuation point, choose the only legal wait; send every illegal state to a rejecting sink:

F (z) = α + (ρ - α) p^{s v_{p} (z)} \frac{z - 1}{z - p^{v_{p} (z)}} .

The remaining problem is whether an even-resultant orbit of this form reaches 1. Bounded primitive denominators already force eventual periodicity. Along every unbounded execution, each maximal Smith step is followed by a locally contracting v ≥ 2 step, but the contraction is measured in a wait-dependent frame and inherited rational height may repay it.

The live obstruction is global amortization: either prove that infinitely many mandatory nonmaximal losses force repetition or a finite certificate, or construct a coefficient-aligned unbounded-denominator orbit that survives them. Exact-order cyclotomic reset-or-cancel laws are available, but no theorem yet extracts enough pairwise-coprime core mass from every such schedule.

No generator-count, rank, punctuation, malformed-word, or illegal-choice problem remains in this architecture. The enemy is the even-resultant unbounded-denominator recurrence, not another supporting coordinate system.

Bookkeeping#

Verification and provenance#

Return compiler

Lean checks the split finite-rank return normal form and the complete mortality equivalence for a rank-one zero return with invertible positive returns.

Three-mode algebra

Lean checks the explicit matrices, return formula, ranks, determinants, projective defect identity, separator, and exact three-state Hankel lower bound.

Guarded dynamics

Lean checks the total projective action, p-adic trap, wait and carry-depth forcing, ready-tail grammar, functional reachability relation, and arbitrary-word converse.

Parity obstruction

Lean checks that adjacent units force an odd prime and that an odd reset resultant excludes physical mortality through the decoded-to-primitive execution lift.

Smith isolation

Lean checks the exact maximal-cancellation identity, its odd target numerator, and the even Smith coordinate forced on every following step.

Exact examples

Lean checks the rational parameters, denominator-cleared integer zero product, and ready nonterminal fixed point.

Transitive axioms

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

Foundational audit

The audit reconstructs the multiplication order, affine poles, trap cases, inverse grammar, concrete certificates, and exact unresolved boundary.

Parity audit

The audit reconstructs the submitted attack, rejects its antichain overclaim, and records the checked master-level wound.

Formal scope#

The matrix identities, rank statements, complete physical mortality equivalence, total projective semantics, p-adic forcing theorems, tail grammar, concrete examples, and exact state lower bound are machine-checked over ℚ. Independent nonzero scaling clears the two physical generators to integer matrices without changing zero products.

The formal result does not prove M₃(2) decidable or undecidable. It proves an exact equivalence for the displayed parametric family, physical immortality for every odd reset resultant, and maximal-step isolation at depth two in the remaining even stratum. No universal source computation has been compiled into the deterministic orbit, and no decision procedure for that orbit is claimed.

The hypotheses are stated at their exact formal strength. The prime need not be separately assumed odd; requiring both α and α−1 to be p-adic units formally excludes residue characteristic two.

Priority#

To our knowledge, after searches through 28 July 2026, the nearest published framework is recurrence-controlled matrix reachability [Hirvensalo et al. 2024]. No located source gives this three-mode return family, its internal separator, the exact valuation trap, or the mortality-to-functional-orbit equivalence. The foundational low-dimensional mortality decomposition and bounded mortality notation are prior art [Bournez–Branicky 2002] [Cassaigne et al. 2014]. “No located source” is limited to publicly discoverable work.

References#

Olivier Bournez and Michael S. Branicky, The Mortality Problem for Matrices of Low Dimensions, Theory of Computing Systems 35(4):433–448, 2002. Low-dimensional mortality and singular-endpoint structure.
Julien Cassaigne, Vesa Halava, Tero Harju, and François Nicolas, Tighter Undecidability Bounds for Matrix Mortality, Zero-in-the-Corner Problems, and More, 2014. Bounded mortality notation and neighboring undecidability bounds.
Mika Hirvensalo, Akitoshi Kawamura, Igor Potapov, and Takao Yuyama, Reachability in Linear Recurrence Automata, Reachability Problems, 2024. Comparative framework for recurrence-indexed matrix reachability.