Polynomial conditioning of the cubic C1 spline Schrödinger Toeplitz family
Let $$\begin{aligned} B_{-1} &= \frac{3}{40}\begin{pmatrix} -1 & 0 \\ -5 & 0 \end{pmatrix}, & B_0 &= \frac{3}{40}\begin{pmatrix} 0 & -5 \\ 16 & -5 \end{pmatrix}, \\ B_1 &= \frac{3}{40}\begin{pmatrix} -5 & 16 \\ -5 & 0 \end{pmatrix}, & B_2 &= \frac{3}{40}\begin{pmatrix} 0 & -5 \\ 0 & -1 \end{pmatrix}, \\ C_{-1} &= \frac{1}{80}\begin{pmatrix} 1 & 0 \\ 7 & 0 \end{pmatrix}, & C_0 &= \frac{1}{80}\begin{pmatrix} 24 & 7 \\ 0 & 25 \end{pmatrix}, \\ C_1 &= \frac{1}{80}\begin{pmatrix} -25 & 0 \\ -7 & -24 \end{pmatrix}, & C_2 &= \frac{1}{80}\begin{pmatrix} 0 & -7 \\ 0 & -1 \end{pmatrix}, \end{aligned}$$ and $B_k = C_k = 0$ for all other integers $k$. For $\rho > 0$ and $n \ge 1$ let $$H_n(\rho) = \bigl(iB_{j-k} - \rho C_{j-k}\bigr)_{j,k=0}^{n-1}$$ be the $2n \times 2n$ block Toeplitz matrix, and let $\kappa_2(H) = \|H\|_2 \|H^{-1}\|_2$ be the spectral condition number, with $\kappa_2(H) = \infty$ for singular $H$. These are the pure block Toeplitz part of the matrices of a space-time isogeometric discretisation of the Schrödinger equation with cubic $C^1$ splines in time, which differ from them by corner perturbations and one extra row and column. For every $\rho > 0$ the determinant of $S(t) = \sum_{k=-1}^{2} (iB_k - \rho C_k)\, t^{k+1}$ has two zeros inside the unit circle, two on it and one outside, counted with multiplicity (Bogoya, Böttcher, Ferrari, Grudsky and Serra-Capizzano), a case in which their criteria for exponential growth of the condition numbers do not apply and their computations suggest at most polynomial growth.
Problem. For every fixed $\rho > 0$, are there constants $K_\rho > 0$, $\alpha_\rho \ge 0$ and $n_\rho$, independent of $n$, such that $$\kappa_2(H_n(\rho)) \le K_\rho\, n^{\alpha_\rho} \qquad \text{for every } n \ge n_\rho?$$
Source: Stated for this family by OpenProblemsInNLA, after Bogoya, Böttcher, Ferrari, Grudsky and Serra-Capizzano (2026), Remark 4.3 and §5.3.
Imported from github.com/ajt60gaibb/OpenProblemsInNLA.
Classification
- Primary
- NA — Numerical Analysis
- Secondary
- FA
- Keywords
- block Toeplitz matrices, condition numbers, isogeometric analysis, OpenProblemsInNLA
References
@misc{bogoya2026,
author = {Bogoya, Manuel and B{\"o}ttcher, Albrecht and Ferrari, Matteo and Grudsky, Sergei M. and Serra-Capizzano, Stefano},
title = {Condition numbers of block {T}oeplitz matrices and stability of space-time {IgA} approximations for the wave and {S}chr{\"o}dinger equations},
year = {2026},
eprint = {2608.24151},
archivePrefix = {arXiv},
}
@misc{openproblemsinnla-mf22,
author = {Townsend, Alex},
title = {{MF-22}: Polynomial conditioning of the cubic C1 spline Schrödinger Toeplitz family},
howpublished = {Open Problems in Numerical Linear Algebra, GitHub repository},
year = {2026},
url = {https://github.com/ajt60gaibb/OpenProblemsInNLA/blob/main/matrix-functions-and-stability/MF-22/README.md},
note = {Read at commit e375a6f, 2026-09-30},
}
Canonical Lean statement
A submission resolves this problem by proving the constant Problem_OP_00097.
namespace RegistryProblems.OP_00097
noncomputable section
open Polynomial
open scoped BigOperators Classical ENNReal
abbrev BlockIndex (n : ℕ) := Fin n × Fin 2
abbrev BlockMatrix (n : ℕ) := Matrix (BlockIndex n) (BlockIndex n) ℂ
/-- The genuine induced complex Euclidean operator norm for the displayed
finite index type; no default entrywise matrix norm is substituted. -/
def spectralNorm {ι : Type*} [Fintype ι] [DecidableEq ι]
(A : Matrix ι ι ℂ) : ℝ :=
‖Matrix.toEuclideanCLM (n := ι) (𝕜 := ℂ) A‖
/-- Singular matrices have infinite condition number, including when the
totalized nonsingular inverse happens to be zero. -/
def conditionNumber {ι : Type*} [Fintype ι] [DecidableEq ι]
(A : Matrix ι ι ℂ) : ℝ≥0∞ :=
if A.det = 0 then ⊤ else ENNReal.ofReal (spectralNorm A * spectralNorm A⁻¹)
/-- Literal coefficient blocks from the original permanent MF-22 statement. -/
def blockB (k : ℤ) : Matrix (Fin 2) (Fin 2) ℝ :=
if k = -1 then (3 / 40 : ℝ) • !![-1, 0; -5, 0]
else if k = 0 then (3 / 40 : ℝ) • !![0, -5; 16, -5]
else if k = 1 then (3 / 40 : ℝ) • !![-5, 16; -5, 0]
else if k = 2 then (3 / 40 : ℝ) • !![0, -5; 0, -1]
else 0
def blockC (k : ℤ) : Matrix (Fin 2) (Fin 2) ℝ :=
if k = -1 then (1 / 80 : ℝ) • !![1, 0; 7, 0]
else if k = 0 then (1 / 80 : ℝ) • !![24, 7; 0, 25]
else if k = 1 then (1 / 80 : ℝ) • !![-25, 0; -7, -24]
else if k = 2 then (1 / 80 : ℝ) • !![0, -7; 0, -1]
else 0
/-- The original pure Toeplitz truncation, with no corner corrections.
The first coordinate is the block index, and offsets use integer subtraction. -/
def toeplitz (ρ : ℝ) (n : ℕ) : BlockMatrix n := fun row col =>
Complex.I * (blockB ((row.1.val : ℤ) - (col.1.val : ℤ)) row.2 col.2 : ℂ) -
(ρ : ℂ) * (blockC ((row.1.val : ℤ) - (col.1.val : ℤ)) row.2 col.2 : ℂ)
/-- OP-00097: Polynomial conditioning of the cubic C1 spline Schrödinger Toeplitz family -/
def _root_.RegistryProblems.Problem_OP_00097 : Prop :=
∀ (ρ : ℝ), 0 < ρ →
∃ K α : ℝ, 0 < K ∧ 0 ≤ α ∧ ∃ n0 : ℕ, 1 ≤ n0 ∧
∀ n : ℕ, n0 ≤ n → (toeplitz ρ n).det ≠ 0 ∧
conditionNumber (toeplitz ρ n) ≤ ENNReal.ofReal (K * Real.rpow (n : ℝ) α)
end
end RegistryProblems.OP_00097
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_00097 theorem resolution : RegistryProblems.Problem_OP_00097 := by sorry
In preprint.toml, mapping the claim to the declaration that establishes it:
[[statements]] label = "Theorem 1" lean = "resolution" latex = "..." problem = "OP-00097" claim = "full"
To disprove it instead, prove the negation and claim "disproof", or "counterexample" if the proof exhibits one:
theorem disproof : ¬ RegistryProblems.Problem_OP_00097 := 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 of the full original MF-22 eventual polynomial-conditioning target, with sufficient exponent 2 and every fixed positive real parameter. All 22 targets passed canonical non-root Linux run 35053254275 at proof commit c701bfeea660473fc31ad9d0c74b76309be3b49f.
For a fixed real $\rho>0$, let $H_n(\rho)$ be the $2n\times2n$ block Toeplitz matrix with blocks $iB_k-\rho C_k$, $-1\le k\le2$, arising from cubic $C^1$ splines in time in a space-time discretisation of the Schrödinger equation. The matrices $H_n(\rho)$ are nonsingular for every sufficiently large $n$, and $\kappa_2(H_n(\rho))\le K_\rho n$ with $K_\rho$ independent of $n$. The linear system is written as a …
Status history
| When | Change | By | Reason |
|---|---|---|---|
| 2026-10-05 | Needs verification → Lean verified | — | Verified here: OpenProblemsInNLA @ e375a6f, MF-22/lean/. |
Citing this problem
This identifier is permanent. It will not change if the problem is solved, reclassified or withdrawn.
OP-00097, "Polynomial conditioning of the cubic C1 spline Schrödinger Toeplitz family", clopen.solutions.