Minimum-Rank and Mortality Bounds for Finite Real Matrix Monoids
partialconfidence 70%
VibeMathed reports this item as partial. VibeMath preserves that report as a source assertion and has not independently authored a plain-language mathematical explanation.
Precise statement
Let $n>0$, and let a family of real $n\times n$ matrices generate a finite entire product monoid $S$. If $s=\min_{X\in S}\operatorname{rank}X$, then some word attains rank $s$ with length at most
$$
B(n,s)=n2^{n-s}-\frac{n(n+1)}2+\frac{s(s-1)}2.
$$
In particular, if $S$ contains zero, a zero word has length at most
$$
B(n,0)=n2^n-\frac{n(n+1)}2=\Theta(n2^n).
$$
Over the rationals, these bounds improve Kiefer–Ryzhikov's (2026) $3^{n^2}$ bounds for mortality and minimum-rank diameter. The mortality bound also improves Almeida–Steinberg's (2009) universal rational bound $(2n-1)^{n^2}-1$ for $n>1$. No finiteness assumption on the generating alphabet is needed. The empty word is allowed and suffices when $s=n$.
The source statement is reproduced for indexing with attribution. Mathematical correctness requires domain-expert or mechanical review. VibeMath has not independently audited statement
fidelity, correctness, priority, or novelty.
What AI did
GPT-6 Astra
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.
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.
For any family of real $n\times n$ matrices generating a finite entire product monoid of minimum rank $s$, some word attains rank $s$ within
$$
B(n,s)=n2^{n-s}-\frac{n(n+1)}2+\frac{s(s-1)}2
$$
letters. The same holds over $\mathbb Q$, without requiring a finite generating alphabet. For mortality, $s=0$, giving a bound of order $n2^n$.
Over $\mathbb Q$, this improves Kiefer–Ryzhikov's (2026) $3^{n^2}$ bounds for mortality and minimum-rank diameter, and Almeida–Steinberg's (2009) mortality bound $(2n-1)^{n^2}-1$ for $n>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.
Known method families
argument (source-reported)
Source-reported tools: argument.
Independent: unknown · difference confidence: 0
What remains uncertain
VibeMath has not independently audited the mathematical statement, proof, or novelty claim.
VibeMath has not independently verified the mathematical claim.
AI-attempt independence and training-data exposure are unknown unless explicitly documented.
VibeMath has not independently audited the mathematical statement, proof, or novelty claim.