A real-valued symbol on a Jordan curve and real Toeplitz spectra
Let $r, s \ge 1$ be integers, let $b(z) = \sum_{k=-r}^{s} b_k z^k$ with $b_k \in \mathbb{C}$ and $b_{-r} b_s \ne 0$, and for $n \ge 1$ let $T_n(b) = (b_{i-j})_{i,j=1}^n$ be the banded Toeplitz matrix generated by $b$, with $b_k = 0$ for $k \notin [-r, s]$. Conversely to the implication below, if $\operatorname{spec}(T_n(b)) \subset \mathbb{R}$ for every $n \ge 1$, then $b$ is real on some Jordan curve in $\mathbb{C} \setminus \{0\}$ (Shapiro and Štampach).
Problem. If there is a Jordan curve $\gamma \subset \mathbb{C} \setminus \{0\}$ such that $b(z) \in \mathbb{R}$ for every $z \in \gamma$, must $\operatorname{spec}(T_n(b)) \subset \mathbb{R}$ for every $n \ge 1$?
Source: Shapiro and Štampach (2019), Theorem 1, implication (ii) ⇒ (iii), whose proof their correction (2023) withdraws.
Imported from github.com/ajt60gaibb/OpenProblemsInNLA.
Classification
- Primary
- SP — Spectral Theory
- Secondary
- CA, NA
- Keywords
- OpenProblemsInNLA, real spectra, Toeplitz matrices
References
@article{shapiro2019,
author = {Shapiro, Boris and {\v{S}}tampach, Franti{\v{s}}ek},
title = {Non-Self-Adjoint {T}oeplitz Matrices Whose Principal Submatrices Have Real Spectrum},
journal = {Constr. Approx.},
volume = {49},
number = {2},
year = {2019},
pages = {191--226},
doi = {10.1007/s00365-017-9408-0},
eprint = {1702.00741},
archivePrefix = {arXiv},
}
@article{shapiro2023,
author = {Shapiro, Boris and {\v{S}}tampach, Franti{\v{s}}ek},
title = {Correction: Non-Self-Adjoint {T}oeplitz Matrices Whose Principal Submatrices Have Real Spectrum},
journal = {Constr. Approx.},
volume = {57},
number = {3},
year = {2023},
pages = {1213--1216},
doi = {10.1007/s00365-022-09614-0},
}
@misc{openproblemsinnla-sp06,
author = {Townsend, Alex},
title = {{SP-06}: A real-valued symbol on a Jordan curve and real Toeplitz spectra},
howpublished = {Open Problems in Numerical Linear Algebra, GitHub repository},
year = {2026},
url = {https://github.com/ajt60gaibb/OpenProblemsInNLA/blob/main/eigenvalues-and-inverse-problems/SP-06/README.md},
note = {Read at commit e375a6f, 2026-09-30},
}
Canonical Lean statement
A submission resolves this problem by proving the constant Problem_OP_00121.
namespace RegistryProblems.OP_00121
noncomputable section
/-- The coefficients of a finite complex Laurent polynomial. -/
abbrev LaurentCoefficients := ℤ →₀ ℂ
def laurentEval (b : LaurentCoefficients) (z : ℂ) : ℂ :=
b.sum (fun k a => a * z ^ k)
/-- The original positive lower and upper bandwidths and nonzero extremes. -/
def hasAdmissibleBand (b : LaurentCoefficients) : Prop :=
∃ r s : ℕ, 1 ≤ r ∧ 1 ≤ s ∧
(∀ k : ℤ, k < -(r : ℤ) ∨ (s : ℤ) < k → b k = 0) ∧
b (-(r : ℤ)) * b (s : ℤ) ≠ 0
def toeplitz (b : LaurentCoefficients) (n : ℕ) :
Matrix (Fin n) (Fin n) ℂ :=
fun i j => b ((i.val : ℤ) - (j.val : ℤ))
/-- A genuine Jordan curve, as the continuous injective image of the unit
circle, avoiding zero and contained in the real locus of the symbol. -/
def hasRealJordanCurve (b : LaurentCoefficients) : Prop :=
∃ γ : Circle → ℂ, Continuous γ ∧ Function.Injective γ ∧
(∀ u, γ u ≠ 0) ∧ (∀ u, (laurentEval b (γ u)).im = 0)
/-- The actual algebra spectrum of every positive finite Toeplitz section. -/
def allFiniteSpectraReal (b : LaurentCoefficients) : Prop :=
∀ n : ℕ, 1 ≤ n → ∀ z : ℂ, z ∈ spectrum ℂ (toeplitz b n) → z.im = 0
/-- OP-00121: A real-valued symbol on a Jordan curve and real Toeplitz spectra -/
def _root_.RegistryProblems.Problem_OP_00121 : Prop :=
∀ b : LaurentCoefficients,
hasAdmissibleBand b → hasRealJordanCurve b → allFiniteSpectraReal b
end
end RegistryProblems.OP_00121
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_00121 theorem resolution : RegistryProblems.Problem_OP_00121 := by sorry
In preprint.toml, mapping the claim to the declaration that establishes it:
[[statements]] label = "Theorem 1" lean = "resolution" latex = "..." problem = "OP-00121" claim = "full"
To disprove it instead, prove the negation and claim "disproof", or "counterexample" if the proof exhibits one:
theorem disproof : ¬ RegistryProblems.Problem_OP_00121 := 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
We construct Laurent polynomials that are real-valued on a Jordan curve surrounding the origin but whose banded Toeplitz matrices have nonreal limiting spectrum. This refutes the weakest surviving form of a conjecture of Shapiro and Štampach, and consequently also the implication to real spectra of all finite sections. The main example $b=h^2$, with $h(z)=z^2+97z+103-10201/z$, has real coefficients and takes values …
Complete negative resolution of the original finite-Toeplitz-spectrum implication, independently reviewed and verified by the actual Linux sandbox, Comparator, permitted-axiom audit and default kernel.
The Laurent polynomial $b(z)=-64z^{-2}+8z^{-1}-128-8z-63z^2-16z^3-z^4$ is real on a star-shaped Jordan curve in $\mathbb C\setminus\{0\}$ enclosing zero, yet its $2\times2$ Toeplitz section has the nonreal eigenvalues $-128\pm8i$. The curve is $\{\rho(t)e^{it}\}$, where $\rho(t)\in(1/2,2)$ is the root of $r^2-1+\tfrac{r^3}{4}\cos t=0$, unique by strict monotonicity in $r$, so that $\rho$ is continuous; the polar form makes the curve injective. On this curve $a(z)=8z^{-1}+8z+z^2$ …
Status history
| When | Change | By | Reason |
|---|---|---|---|
| 2026-10-05 | Needs verification → Lean verified | — | Verified here: OpenProblemsInNLA @ e375a6f, SP-06/lean/. |
Citing this problem
This identifier is permanent. It will not change if the problem is solved, reclassified or withdrawn.
OP-00121, "A real-valued symbol on a Jordan curve and real Toeplitz spectra", clopen.solutions.