VibeMathedMath problems solved with AI
Sign in

An Exponential Mortality Bound for Finite Real Matrix Monoids

Let n>0n>0, and let a family of real n×nn\times n matrices generate a finite entire product monoid containing zero. Then zero is represented by a word of length at mostb(n)=2n−1+(2n−1−1)n(n+1)2=Θ(n22n). b(n)=2^{n-1}+(2^{n-1}-1)\frac{n(n+1)}2 =\Theta(n^2 2^n). The same bound holds for rational matrices, with the same dimension and witnessing word, and no finiteness assumption on the generating alphabet is needed.

Result
Proved(see note)
Status
Partial result
AI contribution
AI-discovered
Method
Argument
Field
Linear algebra
Posed by
Jorge Almeida and Benjamin Steinberg
Year posed
2009
Years open
17y
Solved
2026-09-08
Model
GPT-6 Astra
Vendor
OpenAI
Collaborators
Eugene Gilburg
Verification
Lean-checked, statement unaudited
Publication
Announced
Significance
12 / 100
Disclosed cost
—
Wikipedia
No dedicated article

What was actually shown

For any family (Ma)a∈A(M_a)_{a\in A} of real n×nn\times n matrices whose full word-product setS={Mw:w∈A∗} S=\{M_w:w\in A^*\} is finite and contains zero, there is a zero word of length at most2n−1+(2n−1−1)n(n+1)2. 2^{n-1}+(2^{n-1}-1)\frac{n(n+1)}2.
The proof starts from a singular generator and repeatedly replaces a nonzero word hh by a sandwich hwhhwh whose rank is strictly smaller, with∣w∣≤n(n+1)2. |w|\le \frac{n(n+1)}2. Since rank falls at most n−1n-1 times, the recurrenceLi+1≤2Li+n(n+1)2,L0=1 L_{i+1}\le 2L_i+\frac{n(n+1)}2,\qquad L_0=1 gives the stated bound.

For rational matrices this improves the 3n23^{n^2} mortality bound of Kiefer–Ryzhikov (2026) under the same finite-product promise, and also improves Almeida–Steinberg's universal rational bound(2n−1)n2−1 (2n-1)^{n^2}-1 for n>1n>1.

What the AI did

All original mathematical contributions in the manuscript were produced by AI. The research developed a rank-descent argument for mortality under the finite-product-monoid promise: compressed return semigroups yield finite groups of invertible returns, finite-group averaging supplies an invariant symmetric form, and a symmetric-matrix lift converts rank descent into a short-word detection problem. Iterating the resulting rank-decreasing sandwich gives the final bound. The manuscript and the Lean formalization were also AI-produced, while established ingredients and prior results are separately credited. The human publisher selected and organized the research but does not claim subject-matter review.

Verification

Checked here on 8 September 2026 from the published tree. mortality/lean/SierpinskiFormal/FiniteMortalityBound.lean states exists_short_zero_word_of_finite_real_monoid with the bound 2^(n-1) + (2^(n-1)-1)*n(n+1)/2, under exactly the hypotheses claimed: dimension positive, the range of the word map finite, and some word equal to zero. No sorry and no axiom declarations in that file; Audit.lean prints the axioms for each of the four endpoints. The rational statement is derived from the real one through the cast, so it is a corollary rather than a separate claim. The statement was authored alongside the proof rather than anchored to a canonical tracker, so this takes the statement-unaudited tier. No human mathematical review of the argument is claimed, and none has taken place.

Sources

Submitted by VibeGene on

Changelog3 changes

Discussion1

VibeGene08 Sep 2026, 17:17 UTC

r2 has been published cleaning up the Lean proof. No material changes in the proof or any claims in the manuscript have been made as a result.

0