VibeMathedMath problems solved with AI
Sign in

Minimum-Rank and Mortality Bounds 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 SS. If s=min⁡X∈Srank⁡Xs=\min_{X\in S}\operatorname{rank}X, then some word attains rank ss with length at mostB(n,s)=n2n−s−n(n+1)2+s(s−1)2. B(n,s)=n2^{n-s}-\frac{n(n+1)}2+\frac{s(s-1)}2. In particular, if SS contains zero, a zero word has length at mostB(n,0)=n2n−n(n+1)2=Θ(n2n). B(n,0)=n2^n-\frac{n(n+1)}2=\Theta(n2^n). Over the rationals, these bounds improve Kiefer–Ryzhikov's (2026) 3n23^{n^2} bounds for mortality and minimum-rank diameter. The mortality bound also improves Almeida–Steinberg's (2009) universal rational bound (2n−1)n2−1(2n-1)^{n^2}-1 for n>1n>1. No finiteness assumption on the generating alphabet is needed. The empty word is allowed and suffices when s=ns=n.

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 of real n×nn\times n matrices generating a finite entire product monoid of minimum rank ss, some word attains rank ss withinB(n,s)=n2n−s−n(n+1)2+s(s−1)2 B(n,s)=n2^{n-s}-\frac{n(n+1)}2+\frac{s(s-1)}2 letters. The same holds over Q\mathbb Q, without requiring a finite generating alphabet. For mortality, s=0s=0, giving a bound of order n2nn2^n.

Over Q\mathbb Q, this improves Kiefer–Ryzhikov's (2026) 3n23^{n^2} bounds for mortality and minimum-rank diameter, and Almeida–Steinberg's (2009) mortality bound (2n−1)n2−1(2n-1)^{n^2}-1 for n>1n>1.

The proof uses rank-dependent sandwich descent. Further results give the sharp planar threshold four, additive invariant-flag bounds with sharp small-block examples, and cubic-size compressed witness existence with correct evaluation. Boundedness and individually finite-power generators alone admit no uniform planar mortality bound. General optimality and polynomial-time synthesis are not claimed.

What the AI did

AI produced the manuscript's original mathematical contributions, exposition and Lean formalization. The human publisher directed and organized the research without claiming professional mathematical review. Established methods and prior results are credited separately.

The research developed a rank-descent argument using compressed returns, finite-group averaging and a symmetric-matrix lift. A matrix-valued invariant-form defect gives a rank-dependent short-word detection bound. Iterating the resulting rank-decreasing sandwiches yields the mortality and minimum-rank bounds.

Verification

The site's assessment dated 8 September 2026 concerned the originally submitted mortality theorem. It reported inspection of the formal statement and its hypotheses, no sorry or axiom declarations in the inspected theorem file, and an Audit.lean file exposing endpoint statements and transitive axioms. It assigned the Lean-checked, statement-unaudited tier. No professional human mathematical review was claimed.

The current manuscript is revision r3, published 10 September 2026. Its author-supplied verification supplement records a clean Lean 4.33.1 build of 25 mathematical modules with pinned dependencies, 20 exact statement checks, and endpoint/transitive-axiom audits. The recorded checks passed; the audited endpoints use only propext, Classical.choice and Quot.sound.

The claim map identifies formal support for the real and rational minimum-rank and mortality bounds, planar and invariant-flag results, explicit sharp block examples, boundedness nonuniformity, and compressed-witness existence with evaluator correctness. Prose interpretations and limitations are identified separately. Polynomial-time synthesis is not claimed.

The current supplement does not constitute a new site-administered or independent statement audit. The existing verification tier is retained.

Sources

Submitted by VibeGene on

Changelog6 changes
  • VibeGenechanged Source URL from “https://github.com/egilburg/aimath/tree/mortality-r3/mortality” to “https://github.com/egilburg/aimath/tree/mortality-r4/mortality”, also More links
  • VibeGenecommented
  • VibeGenechanged Name from “An Exponential Mortality Bound for Finite Real Matrix Monoids” to “Minimum-Rank and Mortality Bounds for Finite Real Matrix Monoids”, also Verification note, What the AI did, What was actually shown, Statement, Source URL, More links, Short name
  • VibeGenecommented
  • Rasmus Lindahlapproved this entry
  • VibeGenesubmitted this entry

Discussion2

VibeGene10 Sep 2026, 06:22 UTC

r3 has been published with expanded information. The description and links have been updated.

0
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