Imaginary-part rank in a limiting Green-function matrix equation
Let $C, D, R, P \in \mathbb{C}^{n \times n}$ with $R$ and $P$ Hermitian and $P + \lambda D^* + \lambda^{-1} D$ positive definite for every $\lambda$ with $|\lambda| = 1$. For $\eta > 0$ let $X_\eta$ be the stabilizing solution of $$X + (C^* + i\eta D^*) X^{-1} (C + i\eta D) = R + i\eta P,$$ the nonsingular solution with $\rho(X_\eta^{-1}(C + i\eta D)) < 1$, where $\rho$ is the spectral radius. Assume that $X_0 = \lim_{\eta \downarrow 0} X_\eta$ exists and is nonsingular, and that the quadratic matrix polynomial $\mathcal P_0(\lambda) = \lambda^2 C^* - \lambda R + C$ is regular. The equation arises in Green's function calculations for quantum transport in nanodevices. Guo, Kuo and Lin showed that $X_\eta$ exists and is unique, that the eigenvalues of $\mathcal P_0$ on the unit circle, counted with multiplicity, are even in number, say $2m$, and that $\operatorname{rank}\bigl((X_0 - X_0^*)/(2i)\bigr) \le m$. In an earlier paper they proved equality when $C$ and $R$ are real, $P = I$, $D = 0$ and these eigenvalues are simple.
Problem. If all eigenvalues of $\mathcal P_0$ on the unit circle are simple, and $2m$ is their number, is $$\operatorname{rank}\left(\frac{X_0 - X_0^*}{2i}\right) = m?$$
Source: Guo, Kuo and Lin (2012), the conjecture following Theorem 5.
Imported from github.com/ajt60gaibb/OpenProblemsInNLA.
Classification
- Primary
- NA — Numerical Analysis
- Secondary
- RA
- Keywords
- Green's functions, nonlinear matrix equations, OpenProblemsInNLA, quadratic eigenvalue problems
References
@article{guo2012,
author = {Guo, Chun-Hua and Kuo, Yueh-Cheng and Lin, Wen-Wei},
title = {Numerical solution of nonlinear matrix equations arising from {G}reen's function calculations in nano research},
journal = {J. Comput. Appl. Math.},
volume = {236},
number = {17},
year = {2012},
pages = {4166--4180},
doi = {10.1016/j.cam.2012.05.012},
}
@article{guo2012simax,
author = {Guo, Chun-Hua and Kuo, Yueh-Cheng and Lin, Wen-Wei},
title = {On a Nonlinear Matrix Equation Arising in Nano Research},
journal = {SIAM J. Matrix Anal. Appl.},
volume = {33},
number = {1},
year = {2012},
pages = {235--262},
doi = {10.1137/100814706},
}
@misc{openproblemsinnla-mf18,
author = {Townsend, Alex},
title = {{MF-18}: Imaginary-part rank in a limiting Green-function matrix equation},
howpublished = {Open Problems in Numerical Linear Algebra, GitHub repository},
year = {2026},
url = {https://github.com/ajt60gaibb/OpenProblemsInNLA/blob/main/matrix-functions-and-stability/MF-18/README.md},
note = {Read at commit e375a6f, 2026-09-30},
}
Canonical Lean statement
A submission resolves this problem by proving the constant Problem_OP_00095.
namespace RegistryProblems.OP_00095
noncomputable section
open scoped BigOperators Topology ComplexOrder
abbrev Mat (n : ℕ) := Matrix (Fin n) (Fin n) ℂ
abbrev CPoly := Polynomial ℂ
def regularizedA {n : ℕ} (C D : Mat n) (η : ℝ) : Mat n :=
C + (Complex.I * (η : ℂ)) • D
/-- This is generally not the adjoint of regularizedA. -/
def regularizedB {n : ℕ} (C D : Mat n) (η : ℝ) : Mat n :=
C.conjTranspose + (Complex.I * (η : ℂ)) • D.conjTranspose
def regularizedQ {n : ℕ} (R P : Mat n) (η : ℝ) : Mat n :=
R + (Complex.I * (η : ℂ)) • P
def matrixPolynomial {n : ℕ} (A B Q : Mat n) : Matrix (Fin n) (Fin n) CPoly :=
fun i j => Polynomial.C (B i j) * Polynomial.X ^ 2 -
Polynomial.C (Q i j) * Polynomial.X + Polynomial.C (A i j)
def scalarPencil {n : ℕ} (A B Q : Mat n) : CPoly :=
(matrixPolynomial A B Q).det
def unregularizedPolynomial {n : ℕ} (C R : Mat n) : CPoly :=
scalarPencil C C.conjTranspose R
def CirclePositive {n : ℕ} (P D : Mat n) : Prop :=
∀ lam : ℂ, ‖lam‖ = 1 → (P + lam • D.conjTranspose + lam⁻¹ • D).PosDef
def StrictStable {n : ℕ} (S : Mat n) : Prop :=
∀ lam : ℂ, S.charpoly.IsRoot lam → ‖lam‖ < 1
def IsStabilizingSolution {n : ℕ} (C D R P : Mat n) (η : ℝ) (X : Mat n) : Prop :=
X.det ≠ 0 ∧
X + regularizedB C D η * X⁻¹ * regularizedA C D η = regularizedQ R P η ∧
StrictStable (X⁻¹ * regularizedA C D η)
def circleRootCount (p : CPoly) : ℕ := by
classical
exact (p.roots.filter (fun lam => ‖lam‖ = 1)).card
def SimpleCircleRoots (p : CPoly) : Prop :=
∀ lam : ℂ, ‖lam‖ = 1 → p.IsRoot lam → p.rootMultiplicity lam = 1
def hermitianImaginaryPart {n : ℕ} (X : Mat n) : Mat n :=
((2 * Complex.I : ℂ)⁻¹) • (X - X.conjTranspose)
/-- Only original model assumptions. No rank/count/selection conclusion is a field.
Uniqueness of the given family is not needed for the stronger theorem. -/
def GreenAssumptions {n : ℕ} (C D R P : Mat n) (X : ℝ → Mat n) (X₀ : Mat n) : Prop :=
R.IsHermitian ∧ P.IsHermitian ∧ CirclePositive P D ∧
(∀ η : ℝ, 0 < η → IsStabilizingSolution C D R P η (X η)) ∧
Filter.Tendsto X (nhdsWithin 0 (Set.Ioi 0)) (nhds X₀) ∧
X₀.det ≠ 0 ∧ unregularizedPolynomial C R ≠ 0 ∧
SimpleCircleRoots (unregularizedPolynomial C R)
/-- OP-00095: Imaginary-part rank in a limiting Green-function matrix equation -/
def _root_.RegistryProblems.Problem_OP_00095 : Prop :=
∀ (n : ℕ) [NeZero n] (C D R P : Mat n) (X : ℝ → Mat n) (X₀ : Mat n) (m : ℕ),
GreenAssumptions C D R P X X₀ →
(∀ η : ℝ, 0 < η → ∀ Y : Mat n,
IsStabilizingSolution C D R P η Y → Y = X η) →
circleRootCount (unregularizedPolynomial C R) = 2 * m →
(hermitianImaginaryPart X₀).rank = m
end
end RegistryProblems.OP_00095
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_00095 theorem resolution : RegistryProblems.Problem_OP_00095 := by sorry
In preprint.toml, mapping the claim to the declaration that establishes it:
[[statements]] label = "Theorem 1" lean = "resolution" latex = "..." problem = "OP-00095" claim = "full"
To disprove it instead, prove the negation and claim "disproof", or "counterexample" if the proof exhibits one:
theorem disproof : ¬ RegistryProblems.Problem_OP_00095 := 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
For every complex matrix dimension n≥1 under the original positivity, unique stabilizing family, nonsingular right-limit, regular-pencil and simple-unit-root assumptions, the Hermitian imaginary-part rank equals half the unit-circle root count.
Let $C,D,R,P\in\mathbb{C}^{n\times n}$ with $R,P$ Hermitian and $P+\lambda D^*+\lambda^{-1}D$ positive definite on the unit circle, and let $X_\eta$ be the stabilizing solution of $X+(C^*+i\eta D^*)X^{-1}(C+i\eta D)=R+i\eta P$. If $X_\eta$ tends to a finite nonsingular $X_0$ as $\eta\downarrow0$, the pencil $\lambda^2C^*-\lambda R+C$ is regular and its $2m$ unit-circle eigenvalues are algebraically simple, then $\operatorname{rank}((X_0-X_0^*)/(2i))=m$. Singular $C$ or $D$, unit-circle roots at …
Status history
| When | Change | By | Reason |
|---|---|---|---|
| 2026-10-06 | Needs verification → Lean verified | — | Verified here: OpenProblemsInNLA @ e375a6f, MF-18/lean/. |
Citing this problem
This identifier is permanent. It will not change if the problem is solved, reclassified or withdrawn.
OP-00095, "Imaginary-part rank in a limiting Green-function matrix equation", clopen.solutions.