we-solve (beta)

Math-2200 · mathematics · Algebra

Crouzeix's Conjecture

Status Open · unsolvedmath.comLLM status Open unverified

Statement

Definitions and mathematical statement

Shared notation.
$\mathbb N$, $\mathbb Z$, $\mathbb Q$, $\mathbb R$, and $\mathbb C$ denote the natural numbers, integers, rationals, reals, and complex numbers, respectively. All additional parameters and hypotheses are specified in the question.
Statement recorded in the supplied source.
For a complex square matrix $A$, its numerical range is $W(A)=\{\langle Av,v\rangle:\|v\|=1\}$. If $f$ is analytic on a neighborhood of $W(A)$, must \[\|f(A)\|\leq2\max_{z\in W(A)}|f(z)|\] hold in the Euclidean operator norm? The proposed constant is independent of matrix size.

Formulation references: [S1], [S2].

Short English statement

Does the numerical range control every analytic matrix function with universal constant two?

Sources

Catalogue entry

Statement licence: CC-BY-4.0 · Source file

Contributions 1

Math-2200-A1 · Literature report · LLM-generated · unknown ·

OpenAI claim summary for Math-2200

The result supplies the conclusion in this problem with its displayed hypotheses and quantifiers. The broader statements and applications in the manuscript are kept separate from the particular question above. The supporting results are manuscript 1 (family 325; 2026-09-26), manuscript 2 (family 325; 2026-09-23). The manuscript also gives additional strength beyond the requested conclusion; that excess is not required for this problem's solved-claim label.

Crouzeix's Conjecture

OpenAI's claim

OpenAI presents the following claims relevant to this question, with manuscript numbers following paper order in Sources. In manuscript 1 (family 325; 2026-09-26), the asserted result is that finite matrices obey the sharp constant-two numerical-range bound for matrix-valued polynomials in every coefficient size, including degenerate numerical ranges; In manuscript 2 (family 325; 2026-09-23), the asserted result is that the sharp complete constant-two numerical-range estimate holds for bounded operators without restrictions on Hilbert-space dimension or separability, also for the specified holomorphic and rational calculus.

Mathematical statement of the claimed result

Manuscript 1.
For integers $n,m\ge1$, $d\ge0$, a complex matrix $A\in M_n(\mathbb C)$ and coefficients $B_k\in M_m(\mathbb C)$, let \[ P(z)=\sum_{k=0}^d B_kz^k,\qquad P[A]=\sum_{k=0}^d A^k\otimes B_k, \quad W(A)=\{x^*Ax:x\in\mathbb C^n,\ \|x\|_2=1\}. \] With Hilbert-space operator norms, the claimed complete inequality is \[ \|P[A]\|\le2\max_{z\in W(A)}\|P(z)\|. \] The factor $2$ is asserted sharp uniformly over all three integer parameters. Matrix-valued coefficients are allowed; the scalar polynomial case follows with $m=1$.
Manuscript 2.
For $n,m\ge1$, $A\in M_n(\mathbb C)$, $d\ge0$ and arbitrary $B_0,\ldots,B_d\in M_m(\mathbb C)$, write $P(z)=\sum_jB_jz^j$ and $W(A)=\{x^*Ax:\|x\|_2=1\}$. The claimed complete polynomial inequality is \[ \left\|\sum_{j=0}^dA^j\otimes B_j\right\|\le2\max_{z\in W(A)}\|P(z)\|. \] Hilbert-space operator norms are used, and the constant two is claimed sharp independently of matrix sizes and polynomial degree. The scalar case takes $m=1$.

Outline of the argument

For manuscript 1 (family 325; 2026-09-26), exterior conformal coordinates produce Faber coefficient estimates and a contractive correction kernel. Parseval separation of positive and negative modes controls amplified singular vectors, and enclosing-domain limits include point and segment numerical ranges.

For manuscript 2 (family 325; 2026-09-23), for finite matrices, an optimal positive metric makes the conformal disk coordinate contractive. Endpoint extremal data yield a common continuous boundary density whose ordered comparison forces condition number at most two; domain approximation and finite compressions extend the bound to general operators.

Formal verification

For manuscript 1 (family 325; 2026-09-26), OpenAI lists Lean statements for this assertion: finite matrices obey the sharp constant-two numerical-range bound for matrix-valued polynomials in every coefficient size, including degenerate numerical ranges.

The central assertion is within the documented formal scope; the additional applications retain their own scope limits.

For manuscript 2 (family 325; 2026-09-23), OpenAI lists Lean statements for this assertion: the sharp complete constant-two numerical-range estimate holds for bounded operators without restrictions on Hilbert-space dimension or separability, also for the specified holomorphic and rational calculus.

The central assertion is within the documented formal scope; the additional applications retain their own scope limits.

The linked family Comparator checks are CompleteCrouzeix.lean, CrouzeixHilbert.lean, DirectCrouzeix.lean, HilbertCrouzeix.lean, StructuralCrouzeix.lean.

Their named declarations include OAI.CompleteCrouzeix.main, OAI.CrouzeixHilbert.hilbert, OAI.DirectCrouzeix.complete_crouzeix, OAI.DirectCrouzeix.uniform_sharpness, OAI.HilbertCrouzeix.exists_finite_compression, OAI.HilbertCrouzeix.numericalClosure_geometry, OAI.HilbertCrouzeix.rational_denominator_isUnit, OAI.HilbertCrouzeix.zeroConclusion, OAI.StructuralCrouzeixReference.challenge.

This site has not executed the Lean code. Described statement coverage is not an independent proof check.

Status caveat

The manuscripts were produced by an internal OpenAI model. OpenAI cautions that results without formalization can contain mistakes. This site has not independently checked the proofs; the label records the scope of OpenAI's claim.

Sources

Go to contribution →