Realizing arbitrary polynomial growth exponents by finite matrix families
For a nonempty compact $\mathcal M \subset \mathbb{R}^{d \times d}$ with joint spectral radius $\widehat\rho(\mathcal M) = 1$, let $$g_{\mathcal M}(k) = \max_{A_1, \dots, A_k \in \mathcal M} \|A_k \cdots A_1\|_2$$ be the largest spectral norm of a product of length $k$. If $\mathcal M$ is a single matrix, $g_{\mathcal M}(k)$ lies between positive multiples of $k^j$ for some integer $0 \le j < d$. Varney and Morris showed that the exponents $\alpha$ realised as below by finite families form an additive semigroup containing $0$ and $1/3$.
Problem. For every real $\alpha \ge 0$, are there an integer $d \ge 1$, a finite nonempty $\mathcal M \subset \mathbb{R}^{d \times d}$ with $\widehat\rho(\mathcal M) = 1$, and constants $0 < c \le C < \infty$ such that $$c k^\alpha \le g_{\mathcal M}(k) \le C k^\alpha \qquad \text{for every integer } k \ge 1?$$
Source: Varney and Morris (2025), Question 2.
Imported from github.com/ajt60gaibb/OpenProblemsInNLA.
Classification
- Primary
- DS — Dynamical Systems
- Secondary
- NA, OC
- Keywords
- growth rates, joint spectral radius, matrix products, OpenProblemsInNLA
References
@article{varney2025,
author = {Varney, Jonah and Morris, Ian D.},
title = {On marginal growth rates of matrix products},
journal = {Linear Algebra Appl.},
volume = {709},
year = {2025},
pages = {132--163},
doi = {10.1016/j.laa.2025.01.013},
eprint = {2209.00449},
archivePrefix = {arXiv},
}
@misc{openproblemsinnla-mf12,
author = {Townsend, Alex},
title = {{MF-12}: Realizing arbitrary polynomial growth exponents by finite matrix families},
howpublished = {Open Problems in Numerical Linear Algebra, GitHub repository},
year = {2026},
url = {https://github.com/ajt60gaibb/OpenProblemsInNLA/blob/main/matrix-functions-and-stability/MF-12/README.md},
note = {Read at commit e375a6f, 2026-09-30},
}
Canonical Lean statement
A submission resolves this problem by proving the constant Problem_OP_00093.
namespace RegistryProblems.OP_00093
noncomputable section
open scoped BigOperators Classical
abbrev Square (d : ℕ) := Matrix (Fin d) (Fin d) ℝ
/-- The genuine induced Euclidean operator norm, not an entrywise matrix norm. -/
def spectralNorm {d : ℕ} (A : Square d) : ℝ :=
‖Matrix.toEuclideanCLM (n := Fin d) (𝕜 := ℝ) A‖
/-- Chronological convention: later factors act on the left. -/
def matrixProduct {d : ℕ} (w : List (Square d)) : Square d := w.reverse.prod
/-- All genuine length-n family products. Repeated factors are unrestricted. -/
def wordNorms {d : ℕ} (M : Finset (Square d)) (n : ℕ) : Set ℝ :=
{r | ∃ w : List (Square d), w.length = n ∧
(∀ A ∈ w, A ∈ M) ∧ r = spectralNorm (matrixProduct w)}
/-- The finite maximum is a separate exported attainment obligation. -/
def familyGrowth {d : ℕ} (M : Finset (Square d)) (n : ℕ) : ℝ := sSup (wordNorms M n)
open Filter
open scoped Topology
/-- OP-00093: Realizing arbitrary polynomial growth exponents by finite matrix families -/
def _root_.RegistryProblems.Problem_OP_00093 : Prop :=
∀ (γ : ℝ), 0 ≤ γ →
∃ d : ℕ, 1 ≤ d ∧ ∃ M : Finset (Square d), M.Nonempty ∧
∃ c C : ℝ, 0 < c ∧ c ≤ C ∧
(∀ n : ℕ, 1 ≤ n →
c * Real.rpow (n : ℝ) γ ≤ familyGrowth M n ∧
familyGrowth M n ≤ C * Real.rpow (n : ℝ) γ) ∧
Tendsto (fun n : ℕ => Real.rpow (familyGrowth M n) (1 / (n : ℝ))) atTop (𝓝 1)
end
end RegistryProblems.OP_00093
Formalised by George Stepaniants (Apache-2.0); reviewed by clemens-admin.
Available to match against in: Lean v4.33.1 with Mathlib v4.33.1.
Resolving this problem in Lean
Add the problems package as a dependency, import this problem's module, and prove the constant. Any published revision works.
In lakefile.toml:
[[require]] name = "RegistryProblems" git = "https://github.com/cthalhammer/registry-problems" rev = "753bebc58e3fee845f4fffec7d24e7c8cc2a689a"
In your proof:
import RegistryProblems.OP_00093 theorem resolution : RegistryProblems.Problem_OP_00093 := by sorry
In preprint.toml, mapping the claim to the declaration that establishes it:
[[statements]] label = "Theorem 1" lean = "resolution" latex = "..." problem = "OP-00093" claim = "full"
To disprove it instead, prove the negation and claim "disproof", or "counterexample" if the proof exhibits one:
theorem disproof : ¬ RegistryProblems.Problem_OP_00093 := by sorry
You can also write the statement out in full; the verifier checks it matches up to definitional equality. Partial results and reductions are not matched against this statement.
Resolution claims
Complete formally checked proof for every nonnegative real polynomial growth exponent using a fixed positive-dimensional real matrix pair, all words at every positive length, genuine Euclidean operator norm and the actual nth-root limit one.
For every real $\gamma\geq0$, a finite family of real matrices is constructed whose joint spectral radius is one and whose maximal norm of a product of length $n$ is bounded above and below by positive constant multiples of $n^\gamma$, at every positive integer $n$. For $0<\gamma<1$, two matrices of order six suffice. A rank-two projection reduces arbitrary switching words to …
Status history
| When | Change | By | Reason |
|---|---|---|---|
| 2026-10-05 | Needs verification → Lean verified | — | Verified here: OpenProblemsInNLA @ e375a6f, MF-12/lean/. |
Citing this problem
This identifier is permanent. It will not change if the problem is solved, reclassified or withdrawn.
OP-00093, "Realizing arbitrary polynomial growth exponents by finite matrix families", clopen.solutions.