Pipeline-generated

How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

✓ 25 results · all verified · 23 also independently AI-judged

Every result on this page is machine-checked by a proof checker and read in full and owner-audited; the judge is an additional, independent cross-model AI review of the proofs. The 2 not AI-judged were verified by owner audit (typically over a confirmed judge false positive), not failures.

Verified linear systems and spectral enclosures

1 · Prerequisites

2 · Summary

This page develops verified point and family linear solves, Krawczyk inclusion, real determinant sign checks, Hermitian eigenvalue enclosures, inertia based eigenvalue bisection, and a complex resolvent cover validator. Point residual certificates use rounded operations with explicit error allowances; family certificates use outward interval enclosures. Every validator reports an inconclusive or range status when its numerical checks do not establish the required inequalities. Failed determinant, interval pivot, or inertia checks are not treated as evidence of singularity.

The complex Hermitian results are derived through realification where the available Weyl and inertia interfaces are stated for real symmetric matrices. The contour validator proves a uniform resolvent bound only on its supplied disk cover; it does not count enclosed eigenvalues. Interval dependent claims use the current outward-arithmetic definitions and their DAG soundness theorem; they remain drafts pending independent review.

3 · Logical flowchart

4 · Definitions, theorems and proofs

DefinitionDefinition: AI-adaptedProof: Not applicablejudge pass (gpt-6-luna)Open item page →

The complex induced infinity matrix norm

Definition

For $A = (a_{i j}) \in C^{m \times n}$ with $m, n \geq 1$ , define

∥ A ∥_{\infty, C} : = \max_{1 \leq i \leq m} \sum_{j = 1}^{n} ∣ a_{i j} ∣ .

For a vector $x \in C^{n}$ , define $∥ x ∥_{\infty} : = \max_{j} ∣ x_{j} ∣$ . The absolute value is the complex modulus $∣ u + i v ∣ = \sqrt{u^{2} + v^{2}}$ . The subscript on the matrix norm emphasizes that entries and vectors are complex; this definition is not an appeal to the real-only induced matrix p-norm convention. For square matrices the identity has norm $1$ .

DefinitionDefinition: AI-adaptedProof: Not applicablejudge pass (gpt-6-luna)Open item page →

Residual and near-orthogonality data for an approximate Hermitian eigenbasis

Definition

Let $A$ be a nonempty family of Hermitian matrices in $C^{n \times n}$ , let $V \in C^{n \times n}$ , and let $Θ = diag (θ_{1}, \dots, θ_{n})$ with real $θ_{j}$ . A residual and orthogonality certificate is a tuple of nonnegative numbers $δ, ρ, M_{A}, M_{Θ}, τ$ such that, for every $A \in A$ , $∥ V^{*} V - I ∥_{2} \leq δ < 1, ∥ A V - V Θ ∥_{2} \leq ρ, ∥ A ∥_{2} \leq M_{A}, ∥ Θ ∥_{2} \leq M_{Θ}, 1 - \sqrt{1 - δ} \leq τ .$ The certificate uses exact inequalities or separately verified upper bounds. Its eigenvalue enclosure radius is $η = ρ + (M_{A} + M_{Θ}) τ$ . This definition does not assert that computed residuals or Gram matrices satisfy the bounds; that is a separate certification procedure.

DefinitionDefinition: AI-adaptedProof: Not applicablejudge pass (gpt-6-luna)Open item page →

Verified point and uniform linear residual certificate data

Definition

Let $n \geq 1$ , let $A$ be a nonempty set of matrices in $C^{n \times n}$ , and let $b$ be a nonempty subset of $C^{n}$ . A uniform residual certificate consists of a point matrix $R \in C^{n \times n}$ , a point vector $\hat{x} \in C^{n}$ , and numbers $q, r \geq 0$ such that

∥ I - R A ∥_{2} \leq q, ∥ R (b - A \hat{x}) ∥_{2} \leq r

for every $A \in A$ and $b \in b$ . Here $∥ \cdot ∥_{2}$ is the operator norm induced by the Euclidean vector norm, as in The operator norm is zero on the zero domain and otherwise is max_{||v||=1} ||Tv||. The certificate is usable when $q < 1$ ; in that case its reported error radius is $r / (1 - q)$ . The point-data case is $A = {A}$ and $b = {b}$ .

This definition specifies mathematical upper bounds; it does not specify how a computation establishes them.

LemmaStatement: AI-adaptedProof: AI-adaptedprecheck passjudge pass (gpt-6-luna)Open item page →

Brouwer fixed points exist on every nonempty closed box

Statement

Let $d \geq 0$ and let $X = \prod_{j = 1}^{d} [a_{j}, b_{j}] \subset R^{d}$ be a nonempty closed box, allowing $a_{j} = b_{j}$ . Every continuous map $f : X \to X$ has a fixed point.

Facts & Assumptions

Given: $d$ , a nonempty closed box $X$ as stated, and a continuous $f : X \to X$ .

[F1]

Every continuous self-map of the closed Euclidean unit ball $D^{m}$ has a fixed point for every $m \geq 0$ (Brouwer fixed point theorem).

Proof

1.1givenchooseconstruct

Let $J = {j : a_{j} < b_{j}}$ and $m = ∣ J ∣$ . If $m = 0$ , $X$ is a singleton and its sole point is fixed. If $m > 0$ , deleting the fixed coordinates identifies $X$ with a box $X_{J}$ whose side lengths are all positive. The coordinatewise affine map $T : [- 1, 1]^{m} \to X_{J}$ is a homeomorphism.

2.1step 1.1algebra

For $u \in D^{m} ∖ {0}$ define $h (u) = (∥ u ∥_{2} / ∥ u ∥_{\infty}) u$ and set $h (0) = 0$ . Then $∥ h (u) ∥_{\infty} = ∥ u ∥_{2} \leq 1$ , so $h (D^{m}) \subseteq [- 1, 1]^{m}$ . For $y \neq 0$ in the cube define $h^{- 1} (y) = (∥ y ∥_{\infty} / ∥ y ∥_{2}) y$ and set $h^{- 1} (0) = 0$ ; its Euclidean norm is $∥ y ∥_{\infty} \leq 1$ , and direct substitution shows the formulas are inverse. Both maps are continuous away from zero. At zero, $∥ h (u) ∥_{2} \leq \sqrt{m} ∥ u ∥_{2}$ and $∥ h^{- 1} (y) ∥_{2} = ∥ y ∥_{\infty} \leq ∥ y ∥_{2}$ , so both are continuous there. Thus $h$ is a homeomorphism between the ball and cube.

3.1F1step 1.1step 2.1construct∎

The map $g = (T \circ h)^{- 1} \circ f_{J} \circ (T \circ h) : D^{m} \to D^{m}$ is continuous, where $f_{J}$ is the restriction of $f$ to the non-fixed coordinates after identifying the fixed coordinates. By [F1], $g$ has a fixed point $u$ ; then $(T \circ h) (u)$ is fixed by $f_{J}$ , and restoring the fixed coordinates gives a fixed point of $f$ in $X$ .

LemmaStatement: AI-adaptedProof: AI-adaptedprecheck passjudge pass (gpt-6-luna)Open item page →

Realification preserves Hermitian spectra, norms, and congruence

Statement

For $m, n, p \in N$ and $Z = X + i Y \in C^{m \times n}$ with real $X, Y$ , define its realification

R (Z) = (\begin{array}{cc} X & - Y \\ Y & X \end{array}) \in R^{2 m \times 2 n} .

Use the standard coordinate inner products $⟨ z, w ⟩ = \sum_{j} z_{j} \overline{w_{j}}$ on $C^{k}$ and $⟨ x, y ⟩ = \sum_{j} x_{j} y_{j}$ on $R^{k}$ , with their induced 2-norms. For compatible $Z \in C^{m \times n}$ and $W \in C^{n \times p}$ ,

R (Z W) = R (Z) R (W) .

For any $Z \in C^{m \times n}$ , $R (Z^{*}) = R (Z)^{T}$ . For square $Z \in C^{n \times n}$ , $Z$ is invertible exactly when $R (Z)$ is invertible. If $H = H^{*}$ is Hermitian with eigenvalues $λ_{1}, \dots, λ_{n}$ counted with multiplicity, then $R (H)$ is real symmetric with eigenvalue multiset ${λ_{j}, λ_{j} : 1 \leq j \leq n}$ . For every complex matrix $E \in C^{m \times n}$ , $∥ R (E) ∥_{2} = ∥ E ∥_{2}$ .

Facts & Assumptions

Given: Finite complex matrices $Z, W, E$ of the shapes in the statement and a Hermitian square matrix $H$ .

[F1]

A complex normal endomorphism has an orthonormal eigenbasis (Complex spectral theorem: a normal endomorphism of a finite-dimensional complex inner product space has an orthonormal eigenbasis, and conversely).

[F2]

Every self-adjoint endomorphism is normal (Self-adjoint and normal endomorphisms of a finite-dimensional real or complex inner product space).

[F3]

Rank-nullity implies that an injective endomorphism of a finite-dimensional space is surjective (Rank-nullity: $\dim_{F} V = nullity T + rank T$ ).

[F4]

The operator norm is induced by the vector norms on finite-dimensional real or complex inner-product spaces (The operator norm is zero on the zero domain and otherwise is max_{||v||=1} ||Tv||).

[F5]

The real coordinate inner product is $⟨ x, y ⟩ = \sum_{j} x_{j} y_{j}$ (The Euclidean inner product $⟨ x, y ⟩ = \sum_{k < n} x_{k} y_{k}$ on $R^{n}$ ).

[F6]

Complex inner products are linear in the first variable, conjugate-linear in the second, and induce the norm $∥ z ∥ = \sqrt{⟨ z, z ⟩}$ (Real and complex inner-product spaces and their induced length).

[F7]

In orthonormal coordinate bases, the matrix of the adjoint is the conjugate transpose (In orthonormal bases, the matrix of the adjoint is the conjugate transpose of the matrix).

Proof

1.1givenF6F7algebra

Identify $z = x + i y \in C^{n}$ with $(x, y) \in R^{2 n}$ . For any $Z = X + i Y \in C^{m \times n}$ , direct multiplication gives $R (Z) (x, y) = (ℜ (Z z), ℑ (Z z))$ , so realification respects every compatible product. The displayed inner products make the standard coordinate bases orthonormal, so [F7] gives $Z^{*} = X^{T} - i Y^{T}$ and $R (Z^{*}) = (\begin{array}{cc} X^{T} & Y^{T} \\ - Y^{T} & X^{T} \end{array}) = R (Z)^{T}$ .

2.1F3F4F5F6step 1.1algebra

For $z = x + i y$ , $∥ z ∥_{2}^{2} = \sum_{j} ∣ x_{j} + i y_{j} ∣^{2} = \sum_{j} (x_{j}^{2} + y_{j}^{2}) = ∥ (x, y) ∥_{2}^{2}$ by [F5, F6]. Thus for $n > 0$ the identification bijects the complex and real unit spheres, so the maxima in [F4] coincide for $E$ and $R (E)$ . If $n = 0$ , both operator norms are zero by [F4]. If square $Z$ is invertible, $R (Z^{- 1})$ is an inverse of $R (Z)$ by step 1.1; conversely, if $R (Z)$ is invertible, its kernel is zero, so $Z z = 0$ implies $z = 0$ , and [F3] makes $Z$ invertible.

3.1F1F2F7step 1.1algebra∎

If $n = 0$ , the spectral assertion is immediate. Otherwise, [F7] identifies the Hermitian matrix $H = H^{*}$ with a self-adjoint endomorphism in the standard orthonormal basis; [F2] makes it normal, so [F1] gives $H = U Λ U^{*}$ with $U$ unitary and $Λ = diag (λ_{1}, \dots, λ_{n})$ real. By step 1.1, $R (U)$ is real orthogonal and $R (H) = R (U) R (Λ) R (U)^{T}$ , where $R (Λ) = diag (Λ, Λ)$ . Hence $R (H)$ is real symmetric with each eigenvalue of $H$ repeated twice.

LemmaStatement: AI-adaptedProof: AI-adaptedprecheck passjudge pass (gpt-6-luna)Open item page →

Hermitian eigenvalues lie within a certified Frobenius bound

Statement

If $n \geq 1$ , $A = A^{*} \in C^{n \times n}$ and $M \geq ∥ A ∥_{F}$ , then every eigenvalue $λ$ of $A$ satisfies $∣ λ ∣ \leq M$ . More generally, if a nonempty Hermitian matrix family $A \subseteq C^{n \times n}$ satisfies $∥ A ∥_{F} \leq M$ for all $A \in A$ , then every eigenvalue of every member lies in $[- M, M]$ .

Facts & Assumptions

Given: $A, A, M$ as in the statement.

[F1]

A Hermitian matrix has a unit eigenvector for each eigenvalue (Complex spectral theorem: a normal endomorphism of a finite-dimensional complex inner product space has an orthonormal eigenbasis, and conversely).

[F2]

The operator 2-norm is at most the Frobenius norm (Spectral and Frobenius norms are unitarily invariant, are given by singular values, and satisfy the sharp rank comparison).

[F3]

The operator 2-norm is induced by the Euclidean vector norm (The operator norm is zero on the zero domain and otherwise is max_{||v||=1} ||Tv||).

Proof

1.1givenF1F2F3algebra

Let $A v = λ v$ with $∥ v ∥_{2} = 1$ . Then $∣ λ ∣ = ∥ λ v ∥_{2} = ∥ A v ∥_{2} \leq ∥ A ∥_{2} \leq ∥ A ∥_{F} \leq M$ , using [F1], [F2], and the induced norm definition [F3].

2.1givenF1step 1.1∎

The same calculation applies separately to each $A \in A$ , using its unit eigenvectors and the common bound $M$ . Since Hermitian eigenvalues are real by [F1], all are in $[- M, M]$ .

LemmaStatement: AI-adaptedProof: AI-adaptedprecheck passjudge pass (gpt-6-luna)Open item page →

A Hermitian approximate-eigenpair residual locates a spectral value

Statement

Let $A = A^{*} \in C^{n \times n}$ , $n \geq 1$ , and equip $C^{n}$ with the standard Hermitian inner product $⟨ x, y ⟩ = \sum_{j = 1}^{n} x_{j} \overline{y_{j}}$ and its induced norm $∥ \cdot ∥_{2}$ . For $v \in C^{n} ∖ {0}$ and $θ \in R$ , if $ρ \geq ∥ A v - θ v ∥_{2}$ and $0 < ν \leq ∥ v ∥_{2}$ , then some eigenvalue $λ$ of $A$ satisfies $∣ λ - θ ∣ \leq ρ / ν$ .

Facts & Assumptions

Given: $A, v, θ, ρ, ν$ as in the statement.

[F1]

A Hermitian matrix has an orthonormal eigenbasis with real eigenvalues (Complex spectral theorem: a normal endomorphism of a finite-dimensional complex inner product space has an orthonormal eigenbasis, and conversely).

[F2]

The displayed standard pairing is an inner product: linearity, conjugate symmetry and positive definiteness follow termwise. Its induced norm satisfies $∥ x ∥_{2}^{2} = \sum_{j} ∣ x_{j} ∣^{2}$ , and expansion in any orthonormal basis gives $∥ \sum_{j} c_{j} u_{j} ∥_{2}^{2} = \sum_{j} ∣ c_{j} ∣^{2}$ (Real and complex inner-product spaces and their induced length).

Proof

1.1givenF1F2choosealgebra

Choose an orthonormal eigenbasis $u_{1}, \dots, u_{n}$ with real eigenvalues $λ_{1}, \dots, λ_{n}$ , and write $v = \sum_{j} c_{j} u_{j}$ . Then $A v - θ v = \sum_{j} (λ_{j} - θ) c_{j} u_{j}$ , so [F2] gives $∥ A v - θ v ∥_{2}^{2} = \sum_{j} ∣ λ_{j} - θ ∣^{2} ∣ c_{j} ∣^{2} \geq d^{2} \sum_{j} ∣ c_{j} ∣^{2} = d^{2} ∥ v ∥_{2}^{2}$ , where $d = \min_{j} ∣ λ_{j} - θ ∣$ .

2.1givenstep 1.1algebra∎

Since $v \neq 0$ , $∥ v ∥_{2} > 0$ . Taking nonnegative square roots in step 1.1 and dividing by $∥ v ∥_{2}$ gives $d \leq ∥ A v - θ v ∥_{2} / ∥ v ∥_{2} \leq ρ / ν$ . The finite minimum defining $d$ is attained by some $j$ , and its eigenvalue obeys the required bound.

TheoremStatement: AI-adaptedProof: AI-adaptedprecheck passjudge pass (gpt-6-luna)Open item page →

Certified inertia counts maintain ordered eigenvalue brackets

Statement

Let $n \geq 1$ , let $A$ be a nonempty family of Hermitian $n \times n$ matrices, and let a closed interval $[L, U]$ initially contain every ordered eigenvalue $λ_{k} (A)$ for every $A \in A$ , with eigenvalues listed increasingly. For a query shift $τ$ , suppose the query either returns inconclusive or returns an integer $ν (τ)$ such that every $A \in A$ is nonsingular at $A - τ I$ and exactly $ν (τ)$ of its eigenvalues lie below $τ$ . For each $k \in {1, \dots, n}$ , start with $[L, U]$ and repeat at most $N \in N_{0}$ times: query its midpoint $τ$ ; if $ν (τ) \geq k$ , replace $U$ by $τ$ , and otherwise replace $L$ by $τ$ ; stop when width is at most $ε > 0$ . An inconclusive query returns the current interval without changing it. Every returned interval contains $λ_{k} (A)$ for every $A \in A$ . After $s$ successful queries its width is $(U - L) 2^{- s}$ .

Facts & Assumptions

Given: The initial uniform bracket, tolerance $ε > 0$ , budget $N$ , and the stated query semantics.

[F1]

Hermitian matrices have real ordered eigenvalues (Complex spectral theorem: a normal endomorphism of a finite-dimensional complex inner product space has an orthonormal eigenbasis, and conversely).

[A1]

Every successful query count equals the number of eigenvalues strictly below that shift for every admitted matrix; a successful query excludes a zero eigenvalue at the shift.

Proof

1.1givenF1A1algebra

Fix $k$ . The initial interval contains $λ_{k} (A)$ for every $A$ by hypothesis. At a successful shift $τ$ , if $ν (τ) \geq k$ , then at least $k$ eigenvalues of every $A$ are below $τ$ , so $λ_{k} (A) < τ$ and replacing the upper endpoint by $τ$ preserves every enclosure. If $ν (τ) < k$ , then fewer than $k$ eigenvalues of every $A$ are below $τ$ ; nonsingularity at the shift makes all remaining eigenvalues strictly above $τ$ , so $λ_{k} (A) > τ$ and replacing the lower endpoint preserves every enclosure.

2.1givenstep 1.1algebra∎

Each successful update replaces one endpoint by the midpoint and halves the width. An inconclusive query leaves the already valid interval unchanged. Induction on the number $s$ of successful queries gives width $(U - L) 2^{- s}$ and retains the eigenvalue enclosure in every return branch.

TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passjudge pass (gpt-6-luna)Open item page →

An interval determinant excluding zero certifies nonsingularity and sign

Statement

Let $n \geq 1$ and let $A$ be a nonempty family of real $n \times n$ matrices. Suppose a real interval $D$ contains $\det A$ for every $A \in A$ . If $0 \notin D$ , then every $A \in A$ is nonsingular; if $D$ is positive or negative, its sign is the common determinant sign. If $D = {0}$ , every member is singular. When neither condition holds, the certificate makes no singularity or sign assertion.

Facts & Assumptions

Given: $A$ and a sound real interval determinant enclosure $D$ as stated.

[F1]

The determinant is the finite Leibniz sum for a real square matrix (For $n \geq 1$ , the determinant over a commutative ring by the Leibniz formula, and $∣ \det A ∣$ for a real matrix).

[F2]

A finite square real matrix is invertible exactly when its determinant is nonzero (A finite square real matrix is invertible if and only if its determinant is nonzero).

Proof

1.1givenF1F2

For any $A \in A$ , the assumed enclosure gives $\det A \in D$ . If $0 \notin D$ , then $\det A \neq 0$ , and [F2] makes $A$ nonsingular. If $D$ is a positive or negative interval, every $\det A$ has its corresponding sign.

2.1givenF1F2∎

If $D = {0}$ , then $\det A = 0$ for every $A \in A$ , so [F2] makes every member singular. In the remaining case the stated output is inconclusive and no singularity or sign claim is made.

LemmaStatement: Literature-sourcedProof: AI-adaptedprecheck passjudge pass (gpt-6-luna)Open item page →

Hermitian eigenvalues move by at most the spectral norm perturbation

Statement

Let $A, E \in C^{n \times n}$ be Hermitian, and order their real eigenvalues decreasingly as $λ_{1} (A) \geq \dots \geq λ_{n} (A)$ , $λ_{1} (E) \geq \dots \geq λ_{n} (E)$ , and likewise for $A + E$ . Then for every $1 \leq k \leq n$ ,

∣ λ_{k} (A + E) - λ_{k} (A) ∣ \leq ∥ E ∥_{2} .

Facts & Assumptions

Given: Hermitian $A, E$ and the ordered eigenvalues in the statement.

[F1]

Realification duplicates each Hermitian eigenvalue and preserves operator 2-norms (Realification preserves Hermitian spectra, norms, and congruence).

[F2]

Weyl's two-sided eigenvalue inequalities hold for real self-adjoint sums (Weyl inequalities bound the eigenvalues of a sum of self-adjoint endomorphisms).

[F3]

The operator norm is induced by the Euclidean vector norm (The operator norm is zero on the zero domain and otherwise is max_{||v||=1} ||Tv||).

Proof

1.1givenF1F2

Realify $A$ and $E$ . Their eigenvalues in decreasing order repeat each complex eigenvalue twice, so the $2 k$ -th eigenvalue of $R (A)$ is $λ_{k} (A)$ and similarly for $E$ and $A + E$ . By [F2] with indices $i = 2 k, j = 1$ , the upper Weyl inequality gives $λ_{2 k} (R (A + E)) \leq λ_{2 k} (R (A)) + λ_{1} (R (E))$ . With $i = 2 k, j = 2 n$ , the lower inequality gives $λ_{2 k} (R (A + E)) \geq λ_{2 k} (R (A)) + λ_{2 n} (R (E))$ .

2.1givenF1F3step 1.1algebra∎

For a unit eigenvector $u$ of the Hermitian $E$ , $∣ λ ∣ = ∥ E u ∥_{2} \leq ∥ E ∥_{2}$ by [F3]. Hence $- ∥ E ∥_{2} \leq λ_{2 n} (R (E))$ and $λ_{1} (R (E)) \leq ∥ E ∥_{2}$ by [F1]. Step 1.1 places $λ_{k} (A + E) - λ_{k} (A)$ between these two bounds, proving the result.

LemmaStatement: AI-adaptedProof: AI-adaptedprecheck passjudge pass (gpt-6-luna)Open item page →

Complex Hermitian inertia is invariant under nonsingular congruence

Statement

For a Hermitian $H \in C^{n \times n}$ , define its inertia as $(n_{+} (H), n_{-} (H), n_{0} (H))$ , the counts with multiplicity of positive, negative, and zero eigenvalues. If $S \in C^{n \times n}$ is nonsingular, then

inertia (S^{*} H S) = inertia (H) .

Facts & Assumptions

Given: Hermitian $H$ and nonsingular $S$ as stated.

[F1]

Realification of a Hermitian matrix duplicates each real eigenvalue, and realification of $S^{*} H S$ is the real congruence $R (S)^{T} R (H) R (S)$ ; $R (S)$ is nonsingular (Realification preserves Hermitian spectra, norms, and congruence).

[F2]

For real symmetric matrices, nonsingular congruence preserves positive, negative, and zero inertia counts (Sylvester's law of inertia: every real symmetric form is congruent to $diag (I_{p}, - I_{q}, 0_{r})$ , and $(p, q, r)$ is unique).

Proof

1.1givenF1algebra

By [F1], $R (H)$ and $R (S^{*} H S)$ are real symmetric and the latter equals $R (S)^{T} R (H) R (S)$ with $R (S)$ nonsingular.

2.1step 1.1F1F2algebra∎

Apply [F2] to the realification congruence in step 1.1. The real positive, negative, and zero counts agree; by [F1] each is twice the corresponding complex count, so division by $2$ gives the asserted complex inertia equality.

LemmaStatement: AI-adaptedProof: AI-adaptedprecheck passjudge pass (gpt-6-luna)Open item page →

The complex infinity matrix norm is compatible and submultiplicative

Statement

Use $∥ A ∥_{\infty, C}$ and $∥ x ∥_{\infty}$ from The complex induced infinity matrix norm. For compatible complex matrices and vectors with every row and column dimension positive, $∥ A x ∥_{\infty} \leq ∥ A ∥_{\infty, C} ∥ x ∥_{\infty}, ∥ A B ∥_{\infty, C} \leq ∥ A ∥_{\infty, C} ∥ B ∥_{\infty, C} .$

Facts & Assumptions

Given: Complex matrices $A, B$ and vector $x$ of compatible finite dimensions.

[F1]

Complex absolute value is $∣ u + i v ∣ = \sqrt{u^{2} + v^{2}}$ (The complex induced infinity matrix norm).

[F2]

For real $x_{1}, x_{2}, y_{1}, y_{2}$ , $(x_{1} y_{1} + x_{2} y_{2})^{2} \leq (x_{1}^{2} + x_{2}^{2}) (y_{1}^{2} + y_{2}^{2})$ , since the difference is $(x_{1} y_{2} - x_{2} y_{1})^{2} \geq 0$ .

Proof

1.1F1F2algebra

If $z = x_{1} + i x_{2}$ and $w = y_{1} + i y_{2}$ , then $∣ z w ∣^{2} = (x_{1}^{2} + x_{2}^{2}) (y_{1}^{2} + y_{2}^{2})$ by expansion. Also $∣ z + w ∣^{2} = ∣ z ∣^{2} + ∣ w ∣^{2} + 2 (x_{1} y_{1} + x_{2} y_{2}) \leq (∣ z ∣ + ∣ w ∣)^{2}$ by [F2]. Nonnegativity gives $∣ z w ∣ = ∣ z ∣ ∣ w ∣$ and $∣ z + w ∣ \leq ∣ z ∣ + ∣ w ∣$ .

2.1givenF1step 1.1algebra

For each row $i$ , [F1] and step 1.1 give $∣ (A x)_{i} ∣ \leq \sum_{j} ∣ a_{i j} ∣ ∣ x_{j} ∣ \leq (\sum_{j} ∣ a_{i j} ∣) ∥ x ∥_{\infty}$ . Taking the maximum over $i$ proves compatibility.

3.1step 1.1algebra∎

For each row $i$ , $\sum_{j} ∣ (A B)_{i j} ∣ \leq \sum_{j} \sum_{k} ∣ a_{i k} ∣ ∣ b_{k j} ∣ = \sum_{k} ∣ a_{i k} ∣ \sum_{j} ∣ b_{k j} ∣ \leq (\sum_{k} ∣ a_{i k} ∣) ∥ B ∥_{\infty, C}$ . Taking the maximum over $i$ proves submultiplicativity.

LemmaStatement: AI-adaptedProof: AI-adaptedprecheck passjudge pass (gpt-6-luna)Open item page →

A Neumann defect bounds the inverse norm

Statement

Let $E \in C^{n \times n}$ , $n \geq 1$ , and let $0 \leq q < 1$ satisfy $∥ E ∥_{2} \leq q$ . Then $I - E$ is invertible and

∥ (I - E)^{- 1} ∥_{2} \leq \frac{1}{1 - q} .

Facts & Assumptions

Given: $E, q, n$ as in the statement.

[F1]

If $∥ X ∥_{2} < 1$ , then $I + X$ is invertible (A finite matrix within unit distance of the identity is invertible).

[F2]

The operator norm is submultiplicative (The operator norm is submultiplicative and satisfies ||T^*T|| = ||T||^2).

[F3]

The operator norm is induced by the Euclidean vector norm (The operator norm is zero on the zero domain and otherwise is max_{||v||=1} ||Tv||).

Proof

1.1givenF1

Since $∥ - E ∥_{2} = ∥ E ∥_{2} \leq q < 1$ , [F1] gives that $T = (I - E)^{- 1}$ exists.

2.1givenF2F3step 1.1algebra∎

Put $S_{N} = \sum_{k = 0}^{N} E^{k}$ . By induction and [F2], $∥ E^{k} ∥_{2} \leq q^{k}$ , so $∥ S_{N} ∥_{2} \leq \sum_{k = 0}^{N} q^{k} = (1 - q^{N + 1}) / (1 - q)$ by [F3]. The finite identity $(I - E) S_{N} = I - E^{N + 1}$ , multiplied on the left by $T$ , gives $S_{N} = T - T E^{N + 1}$ and hence $T = S_{N} + T E^{N + 1}$ . By the triangle inequality from [F3] and submultiplicativity [F2], $(1 - q^{N + 1}) ∥ T ∥_{2} \leq ∥ S_{N} ∥_{2} \leq (1 - q^{N + 1}) / (1 - q)$ . Since $q^{N + 1} < 1$ , division gives $∥ T ∥_{2} \leq (1 - q)^{- 1}$ . This proves the inverse norm bound without taking a limit of matrices.

LemmaStatement: AI-adaptedProof: AI-adaptedprecheck passjudge pass (gpt-6-luna)Open item page →

A Hermitian two-by-two pivot inertia is determined by determinant and trace signs

Statement

Let $D \in C^{2 \times 2}$ be Hermitian, and let $Δ = \det D$ and $t = tr D$ , using the matrix determinant and trace. Here $inertia (D)$ denotes the counts, with multiplicity, of its positive, negative, and zero eigenvalues (Complex Hermitian inertia is invariant under nonsingular congruence). Then $Δ$ and $t$ are real. If $Δ < 0$ , then $inertia (D) = (1, 1, 0)$ . If $Δ > 0$ and $t > 0$ , then $inertia (D) = (2, 0, 0)$ ; if $Δ > 0$ and $t < 0$ , then $inertia (D) = (0, 2, 0)$ . No conclusion is asserted when $Δ = 0$ or when $Δ > 0$ and $t = 0$ .

Facts & Assumptions

Given: A Hermitian matrix $D \in C^{2 \times 2}$ .

[F1]

A Hermitian endomorphism is normal (Self-adjoint and normal endomorphisms of a finite-dimensional real or complex inner product space), and every finite-dimensional complex normal endomorphism has an orthonormal eigenbasis (Complex spectral theorem: a normal endomorphism of a finite-dimensional complex inner product space has an orthonormal eigenbasis, and conversely).

[F2]

Similar matrices have the same characteristic polynomial (Similar matrices have the same characteristic polynomial).

[F3]

The matrix characteristic polynomial is $χ_{D} (x) = \det (x I - D)$ (For $A \in M_{n} (F)$ , the characteristic polynomial is $χ_{A} (x) = \det (x I_{n} - A)$ when $n \geq 1$ , with $χ_{A} (x) = 1$ for the unique $0 \times 0$ matrix).

[F4]

The determinant of a triangular matrix is the product of its diagonal entries (The determinant of a triangular matrix is the product of its diagonal entries).

[F5]

For the two-by-two matrix $D$ , the constant coefficient of $χ_{D}$ is $\det D$ and its $x$ coefficient is $- tr D$ ( $χ_{A} (x)$ is monic of degree $n$ ; for $n \geq 1$ its $x^{n - 1}$ coefficient is $- tr (A)$ and its constant coefficient is $(- 1)^{n} \det (A)$ , while $χ_{0 \times 0} = 1$ ).

[F6]

The matrix determinant is the finite Leibniz sum (For $n \geq 1$ , the determinant over a commutative ring by the Leibniz formula, and $∣ \det A ∣$ for a real matrix).

[F7]

The matrix trace is the sum of the diagonal entries (The trace $tr (A)$ as the sum of the diagonal entries).

[F8]

Inertia is the triple of positive, negative, and zero eigenvalue counts with multiplicity (Complex Hermitian inertia is invariant under nonsingular congruence).

Proof

1.1givenF1F2F3F4F6choosealgebra

By [F1], choose a unitary $U$ and real eigenvalues $λ_{1}, λ_{2}$ such that $D = U diag (λ_{1}, λ_{2}) U^{*}$ . The matrices $D$ and $diag (λ_{1}, λ_{2})$ are similar, so [F2] gives the same characteristic polynomial. By [F3], [F4] and the determinant definition [F6], $χ_{D} (x) = (x - λ_{1}) (x - λ_{2}) = x^{2} - (λ_{1} + λ_{2}) x + λ_{1} λ_{2}$ .

2.1F5F7step 1.1algebra

By [F5], the constant and linear coefficients of $χ_{D}$ are $Δ$ and $- t$ . The matrix trace is the diagonal sum by [F7]. Comparing with the factorization in step 1.1 gives $Δ = λ_{1} λ_{2}$ and $t = λ_{1} + λ_{2}$ , so both are real.

3.1givenF8step 2.1algebra∎

If $Δ < 0$ , the two real eigenvalues have opposite signs, so there is one positive and one negative eigenvalue. If $Δ > 0$ , their product is positive and neither is zero, so they have the same sign; their sum $t$ is then positive exactly when both are positive and negative exactly when both are negative. By [F8], these sign counts are the three stated inertia triples.

LemmaStatement: AI-adaptedProof: AI-adaptedprecheck passjudge pass (gpt-6-luna)Open item page →

A complex infinity-norm defect bounds the inverse norm

Statement

Let $E \in C^{n \times n}$ , $n \geq 1$ , and $0 \leq q < 1$ satisfy $∥ E ∥_{\infty, C} \leq q$ . Then $I - E$ is invertible and

∥ (I - E)^{- 1} ∥_{\infty, C} \leq \frac{1}{1 - q} .

Facts & Assumptions

Given: $E, q, n$ as in the statement.

[F1]

The complex infinity matrix norm is submultiplicative (The complex infinity matrix norm is compatible and submultiplicative).

[F2]

Its vector norm is the maximum coordinate modulus and its matrix norm is the maximum absolute row sum; in particular $∥ I ∥_{\infty, C} = 1$ and $∣ Y_{i j} ∣ \leq ∥ Y ∥_{\infty, C} \leq n \max_{i, j} ∣ Y_{i j} ∣$ (The complex induced infinity matrix norm).

[F3]

An injective endomorphism of a finite-dimensional vector space is invertible (Rank-nullity: $\dim_{F} V = nullity T + rank T$ ).

Proof

1.1givenF1F3algebra

If $(I - E) x = 0$ , then $x = E x$ . The vector compatibility bound in [F1] gives $∥ x ∥_{\infty} \leq q ∥ x ∥_{\infty}$ , so $x = 0$ because $q < 1$ . Thus $I - E$ is injective, and [F3] makes it invertible; put $T = (I - E)^{- 1}$ .

2.1givenF1F2step 1.1algebra∎

Define $S_{N} = \sum_{k = 0}^{N} E^{k}$ . By induction and [F1], $∥ E^{k} ∥_{\infty, C} \leq q^{k}$ . The row-sum definition [F2] gives $∥ I ∥_{\infty, C} = 1$ and the triangle inequality, so $∥ S_{N} ∥_{\infty, C} \leq (1 - q^{N + 1}) / (1 - q)$ . The identity $(I - E) S_{N} = I - E^{N + 1}$ , multiplied on the left by $T$ from step 1.1, gives $S_{N} = T - T E^{N + 1}$ and hence $T = S_{N} + T E^{N + 1}$ . By [F2] and submultiplicativity [F1], $(1 - q^{N + 1}) ∥ T ∥_{\infty, C} \leq ∥ S_{N} ∥_{\infty, C} \leq (1 - q^{N + 1}) / (1 - q)$ . Since $q^{N + 1} < 1$ , division proves the asserted bound.

LemmaStatement: AI-adaptedProof: AI-adaptedprecheck passjudge pass (gpt-6-luna)Open item page →

Block LDL congruence adds the Hermitian pivot inertias

Statement

Let $k \geq 1$ , $m \geq 0$ , and let $H = (\begin{array}{cc} D & B^{*} \\ B & C \end{array}) \in C^{(k + m) \times (k + m)}$ be Hermitian, where $D = D^{*} \in C^{k \times k}$ is nonsingular, $B \in C^{m \times k}$ , and $C = C^{*} \in C^{m \times m}$ . Define the Schur complement $S = C - B D^{- 1} B^{*}$ . Inertia triples are added coordinatewise, and the $0 \times 0$ matrix has inertia $(0, 0, 0)$ . Then

inertia (H) = inertia (D) + inertia (S),

where the triples are added coordinatewise.

Facts & Assumptions

Given: $H, D, B, C, S$ as in the statement.

[F1]

Nonsingular complex congruence preserves Hermitian inertia (Complex Hermitian inertia is invariant under nonsingular congruence).

[F2]

Proof

1.1givenalgebra

Set $L = (\begin{array}{cc} I & 0 \\ B D^{- 1} & I \end{array})$ . It is invertible, with inverse $(\begin{array}{cc} I & 0 \\ - B D^{- 1} & I \end{array})$ . Direct block multiplication gives $H = L (\begin{array}{cc} D & 0 \\ 0 & S \end{array}) L^{*}$ , so $H$ is congruent to $diag (D, S)$ .

2.1givenF1F2step 1.1algebra∎

Since $D = D^{*}$ and $D$ is invertible, $(D^{- 1})^{*} = (D^{*})^{- 1} = D^{- 1}$ . Therefore $(B D^{- 1} B^{*})^{*} = B D^{- 1} B^{*}$ , and $C = C^{*}$ gives $S^{*} = S$ . By [F1], $inertia (H) = inertia (diag (D, S))$ . If $m = 0$ , the trailing block is empty and its inertia is $(0, 0, 0)$ by the stated convention. If $m > 0$ , [F2] diagonalizes the Hermitian matrices $D$ and $S$ separately; concatenating their orthonormal eigenbases diagonalizes the block diagonal matrix, so its positive, negative and zero counts are the sums of the corresponding counts for $D$ and $S$ .

TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passjudge pass (gpt-6-luna)Open item page →

Krawczyk inclusion gives solutions and contraction gives uniqueness

Statement

Let $n \geq 1$ , let $A \subseteq C^{n \times n}$ and $b \subseteq C^{n}$ be nonempty, let $X$ be a nonempty closed complex rectangle box in $C^{n} ≅ R^{2 n}$ , let $x_{0} \in X$ , and let the point matrix $R$ be nonsingular. For each fixed $A \in A, b \in b$ , define

Φ_{A, b} (x) = x - R (A x - b)

and

K^{*} (X) = {x_{0} - R (A x_{0} - b) + (I - R A) (x - x_{0}) : A \in A, b \in b, x \in X} .

If $K^{*} (X) \subseteq X$ , then every admitted pair $(A, b)$ has a solution in $X$ . If in addition a number $q < 1$ satisfies $∥ I - R A ∥_{\infty, C} \leq q$ for every $A \in A$ , that solution is unique in $X$ for each fixed pair.

Facts & Assumptions

Given: The families, box, center, and nonsingular $R$ in the statement.

[F1]

Every continuous self-map of a closed box has a fixed point (Brouwer fixed points exist on every nonempty closed box).

[F2]

The complex infinity matrix norm is compatible with multiplication by vectors (The complex infinity matrix norm is compatible and submultiplicative).

[F3]

The vector infinity norm is the maximum coordinate modulus (The complex induced infinity matrix norm).

Proof

1.1givenF1algebra

Fix any $A \in A, b \in b$ . Algebra gives $Φ_{A, b} (x) = x_{0} - R (A x_{0} - b) + (I - R A) (x - x_{0})$ , so $K^{*} (X) \subseteq X$ implies $Φ_{A, b} (X) \subseteq X$ . The affine map $Φ_{A, b}$ is continuous on the closed box, so [F1] gives a fixed point $x \in X$ . Since $R$ is nonsingular, $Φ_{A, b} (x) = x$ is equivalent to $A x = b$ .

2.1givenF2F3step 1.1∎

If $x, y \in X$ both solve the same system, then both are fixed points and $x - y = (I - R A) (x - y)$ . By [F2] and [F3], $∥ x - y ∥_{\infty} \leq q ∥ x - y ∥_{\infty}$ . Since the vector infinity norm [F3] vanishes only at the zero vector and $q < 1$ , $x = y$ . This proves uniqueness for that pair; the pair was arbitrary.

TheoremStatement: AI-adaptedProof: AI-adaptedprecheck passjudge pass (gpt-6-luna)Open item page →

Near-orthonormal residual data enclose all ordered Hermitian eigenvalues

Statement

Let $n \geq 1$ and let $(V, Θ, δ, ρ, M_{A}, M_{Θ}, τ)$ be a residual and orthogonality certificate for a nonempty family $A$ of Hermitian matrices in $C^{n \times n}$ . Sort the diagonal entries of $Θ$ increasingly as $θ_{(1)} \leq \dots \leq θ_{(n)}$ . Then every $A \in A$ has ordered eigenvalues $λ_{1} (A) \leq \dots \leq λ_{n} (A)$ satisfying

∣ λ_{k} (A) - θ_{(k)} ∣ \leq ρ + (M_{A} + M_{Θ}) τ, 1 \leq k \leq n .

Facts & Assumptions

Given: The certificate and all bounds in Residual and near-orthogonality data for an approximate Hermitian eigenbasis.

[F1]

Hermitian matrices are unitarily diagonalizable with real eigenvalues (Complex spectral theorem: a normal endomorphism of a finite-dimensional complex inner product space has an orthonormal eigenbasis, and conversely).

[F2]

A non-negative operator has a unique non-negative square root (A non-negative operator has a unique non-negative square root).

[F3]

Complex Hermitian eigenvalues change by at most the spectral norm of a Hermitian perturbation (Hermitian eigenvalues move by at most the spectral norm perturbation).

[F4]

Rank-nullity converts injectivity of a square endomorphism into invertibility (Rank-nullity: $\dim_{F} V = nullity T + rank T$ ).

[F5]

The operator norm is induced by the Euclidean norm and is unchanged by unitary factors (The operator norm is zero on the zero domain and otherwise is max_{||v||=1} ||Tv||).

[F6]

Cauchy–Schwarz gives $∣ x^{*} y ∣ \leq ∥ x ∥_{2} ∥ y ∥_{2}$ in a complex inner-product space (Cauchy–Schwarz: $∣ ⟨ u, v ⟩ ∣ \leq ∥ u ∥ ∥ v ∥$ , with equality exactly for linearly dependent vectors).

[F7]

The induced operator norm is submultiplicative (The operator norm is submultiplicative and satisfies ||T^*T|| = ||T||^2).

Proof

1.1givenF1F2F5F6algebra

Put $G = V^{*} V$ . For every unit vector $x$ , [F6] gives $∣ x^{*} (G - I) x ∣ \leq ∥ x ∥_{2} ∥ (G - I) x ∥_{2} \leq ∥ G - I ∥_{2} \leq δ$ by [F5], so all eigenvalues $μ$ of the Hermitian $G$ lie in $[1 - δ, 1 + δ]$ . Since $δ < 1$ , $G$ is positive definite. By [F1] and [F2] it has a positive square root $H$ ; its eigenvalues are $\sqrt{μ} > 0$ , so $H$ is invertible.

2.1givenF1F2F4F5step 1.1algebra

Set $Q = V H^{- 1}$ . Then $Q^{*} Q = H^{- 1} V^{*} V H^{- 1} = I$ . Thus $Q$ is injective and [F4] makes the square matrix $Q$ invertible, so $Q$ is unitary. The eigenvalues of $H$ lie between $\sqrt{1 - δ}$ and $\sqrt{1 + δ}$ , hence $∥ V - Q ∥_{2} = ∥ Q (H - I) ∥_{2} = ∥ H - I ∥_{2} \leq 1 - \sqrt{1 - δ} \leq τ$ . For the upper deviation, $\sqrt{1 + δ} - 1 \leq 1 - \sqrt{1 - δ}$ because $\sqrt{1 + δ} + \sqrt{1 - δ} \leq 2$ . Unitary invariance in [F5] justifies the norm equality.

3.1givenF5F7step 2.1algebra

For each $A \in A$ , the residual identity $A Q - Q Θ = A (Q - V) + (A V - V Θ) + (V - Q) Θ$ and certificate bounds give $∥ A Q - Q Θ ∥_{2} \leq M_{A} τ + ρ + τ M_{Θ} = η$ . By the triangle inequality and submultiplicativity [F7], each product term in the identity is bounded by its factor norms, giving the displayed estimate. Since $Q$ is unitary, [F5] gives that $Q^{*} A Q$ has the same ordered eigenvalues as $A$ and, using [F7], $∥ Q^{*} A Q - Θ ∥_{2} = ∥ Q^{*} (A Q - Q Θ) ∥_{2} \leq η$ .

4.1givenF3step 3.1algebra∎

Both $Q^{*} A Q$ and $Θ$ are Hermitian. Their eigenvalues are ordered increasingly in the statement of the enclosure, whereas [F3] uses decreasing order; reversing both lists sends index $k$ to $n + 1 - k$ , so the same absolute-difference bound holds at each increasing index. Applying [F3] to their difference gives $∣ λ_{k} (A) - θ_{(k)} ∣ \leq η$ for every $k$ . The family bounds are uniform, so the same intervals hold for every $A \in A$ .

TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passjudge pass (gpt-6-luna)Open item page →

A uniform approximate inverse and residual enclose every linear solution

Statement

If $(R, \hat{x}, q, r)$ is usable uniform residual certificate data for nonempty $A \subseteq C^{n \times n}$ and $b \subseteq C^{n}$ , then for every $A \in A$ and $b \in b$ , the equation $A x = b$ has a unique solution $x_{A} (b)$ and

∥ x_{A} (b) - \hat{x} ∥_{2} \leq \frac{r}{1 - q} .

Facts & Assumptions

Given: The uniform certificate data, with $q < 1$ .

[F1]

For $∥ E ∥_{2} \leq q < 1$ , $I - E$ is invertible and $∥ (I - E)^{- 1} ∥_{2} \leq (1 - q)^{- 1}$ (A Neumann defect bounds the inverse norm).

[F2]

The operator 2-norm is compatible with composition (The operator norm is submultiplicative and satisfies ||T^*T|| = ||T||^2).

[F3]

Rank-nullity makes an injective or surjective endomorphism of a finite-dimensional space invertible (Rank-nullity: $\dim_{F} V = nullity T + rank T$ ).

[F4]

The operator 2-norm is induced by the Euclidean vector norm (The operator norm is zero on the zero domain and otherwise is max_{||v||=1} ||Tv||).

Proof

1.1givenF1F3algebra

Fix any $A \in A$ and $b \in b$ , and put $E = I - R A$ . Certificate data give $∥ E ∥_{2} \leq q < 1$ , so $R A = I - E$ is invertible by [F1]. If $A x = 0$ , then $R A x = 0$ and injectivity of $R A$ gives $x = 0$ ; hence $A$ is injective and invertible by [F3]. Also $R A$ is surjective, so $R$ is surjective and invertible by [F3]. Thus $A x = b$ has a unique solution.

2.1givenF1F2F4step 1.1∎

For that solution, $R A (x_{A} (b) - \hat{x}) = R (b - A \hat{x})$ . The matrix and vector norms are the induced Euclidean norms by [F4], so [F2] applies; since $R A = I - E$ , certificate data and [F1] imply $∥ x_{A} (b) - \hat{x} ∥_{2} \leq ∥ (I - E)^{- 1} ∥_{2} ∥ R (b - A \hat{x}) ∥_{2} \leq r / (1 - q)$ . Every choice of $A, b$ was arbitrary, proving the uniform conclusion.

TheoremStatement: AI-adaptedProof: AI-adaptedprecheck passjudge pass (gpt-6-luna)Open item page →

Diskwise Neumann certificates bound a complex matrix resolvent

Statement

Let $n \geq 1$ , let $Γ$ be a nonempty finite union of closed line segments in $C$ , let $A \subseteq C^{n \times n}$ be nonempty, and let $A_{0} \in C^{n \times n}$ . Each segment of $Γ$ is assigned to one of finitely many disks $D_{j} = {z : ∣ z - z_{j} ∣ \leq r_{j}}$ whose radius is $r_{j} \geq 0$ and whose disk contains both endpoints of that segment. For each disk there are $R_{j} \in C^{n \times n}$ and nonnegative bounds $e_{j}, δ_{A}, s_{j}$ satisfying $e_{j} \geq ∥ I - R_{j} (z_{j} I - A_{0}) ∥_{\infty, C}, δ_{A} \geq \sup_{A \in A} ∥ A - A_{0} ∥_{\infty, C}, s_{j} \geq ∥ R_{j} ∥_{\infty, C} .$ If $q_{j} = e_{j} + s_{j} (r_{j} + δ_{A}) < 1$ for each $j$ , then every $z \in Γ$ and $A \in A$ make $z I - A$ invertible, and $∥ (z I - A)^{- 1} ∥_{\infty, C} \leq \max_{j} \frac{s_{j}}{1 - q_{j}} .$ The theorem bounds the resolvent on the supplied contour cover; it does not count enclosed eigenvalues or certify a nonnormal eigenvalue disk from a residual.

Facts & Assumptions

Given: $Γ, A, A_{0}, D_{j}, R_{j}, e_{j}, δ_{A}, s_{j}$ and $q_{j}$ as in the statement.

[F1]

A defect of complex infinity norm at most $q < 1$ has inverse norm at most $(1 - q)^{- 1}$ (A complex infinity-norm defect bounds the inverse norm).

[F2]

The complex infinity matrix norm is compatible with products (The complex infinity matrix norm is compatible and submultiplicative).

[F3]

A product of square matrices is nonsingular only if each factor is nonsingular, by rank-nullity (Rank-nullity: $\dim_{F} V = nullity T + rank T$ ).

[F4]

The complex infinity matrix norm is the maximum absolute row sum, so $∥ I ∥_{\infty, C} = 1$ (The complex induced infinity matrix norm).

Proof

1.1givenalgebra

Each segment of $Γ$ has both endpoints in its assigned disk. A disk is convex, so the segment between its endpoints lies in the disk; the finite assignments therefore cover all of $Γ$ .

1.2givenF1F2F4algebra

Fix a disk, $z \in D_{j}$ , and $A \in A$ . The exact identity $I - R_{j} (z I - A) = I - R_{j} (z_{j} I - A_{0}) - R_{j} ((z - z_{j}) I - (A - A_{0}))$ and [F2] give $∥ I - R_{j} (z I - A) ∥_{\infty, C} \leq e_{j} + s_{j} (∣ z - z_{j} ∣ + ∥ A - A_{0} ∥_{\infty, C}) \leq q_{j} < 1$ . [F1] applies to $M = R_{j} (z I - A) = I - E$ with $E = I - M$ , giving $∥ M^{- 1} ∥_{\infty, C} \leq (1 - q_{j})^{- 1}$ . Here [F4] gives $∥ (z - z_{j}) I ∥_{\infty, C} = ∣ z - z_{j} ∣$ , and the row-sum norm's triangle inequality and compatibility [F2, F4] justify the defect estimate.

2.1givenF1F2F3F4step 1.1step 1.2algebra∎

By [F4], $∥ I ∥_{\infty, C} = 1$ . Since $M = R_{j} (z I - A)$ is nonsingular, both square factors are nonsingular by [F3]. Then $(z I - A)^{- 1} = M^{- 1} R_{j}$ , so [F2] gives $∥ (z I - A)^{- 1} ∥_{\infty, C} \leq s_{j} / (1 - q_{j})$ . The disk cover from step 1.1 yields the maximum bound on all of $Γ$ , uniformly in $A$ .

AlgorithmAlgorithm: Literature-sourcedProof: Not applicablejudge pass (gpt-6-luna)Open item page →

Finite complex contour resolvent validator with cover and inconclusive statuses

Definition

Input $n \geq 1$ and a nonempty finite union of complex line segments $Γ$ , with each segment assigned to a proposed disk $D_{j} = B (z_{j}, r_{j})$ ; a nonempty matrix family $A \subseteq C^{n \times n}$ enclosed by complex rectangles; a point center matrix $A_{0} \in C^{n \times n}$ ; and proposed point preconditioners $R_{j} \in C^{n \times n}$ . All segment endpoints, disk centers, radii and point matrices are exact dyadics.

For each assigned segment verify that both endpoints lie in its disk by exact rational comparison of squared distances with $r_{j}^{2}$ . Evaluate outward bounds $e_{j} \geq ∥ I - R_{j} (z_{j} I - A_{0}) ∥_{\infty, C}, δ_{A} \geq \sup_{A \in A} ∥ A - A_{0} ∥_{\infty, C}, s_{j} \geq ∥ R_{j} ∥_{\infty, C}$ using the complex rectangle operations and row sums of outward modulus bounds. If any check or operation cannot be completed, return inconclusive.
Outward-compute $q_{j} = e_{j} + s_{j} (r_{j} + δ_{A})$ . Require $q_{j} < 1$ for every disk and compute an outward upper bound $m \geq \max_{j} s_{j} / (1 - q_{j})$ . If a strict inequality or division cannot be certified, return inconclusive; otherwise return certified-resolvent-cover with the disk assignments and $m$ .

The validated endpoint cover covers each whole segment because disks are convex. Success certifies a resolvent bound on this supplied contour cover, but this procedure does not count enclosed eigenvalues or validate contour topology.

AlgorithmAlgorithm: Literature-sourcedProof: Not applicablejudge pass (gpt-6-luna)Open item page →

Outward Leibniz determinant sign and nonsingularity certifier

Definition

Input $n \geq 1$ and a nonempty family of real $n \times n$ matrices contained in a box of real intervals. Evaluate the determinant's finite Leibniz expression

\det A = \sum_{σ \in S_{n}} sgn (σ) \prod_{i = 1}^{n} a_{i, σ (i)}

as an outward interval DAG, retaining every permutation term and reporting the final interval $D$ . If any operation returns overflow or another non-finite status, return inconclusive.

If $0 \notin D$ , return nonsingular and the sign of $D$ . If $D = {0}$ , return all-singular. In every other case return inconclusive. This finite procedure has factorially many permutation terms; no efficiency or determinant sign is claimed when zero remains in the enclosure.

AlgorithmAlgorithm: Literature-sourcedProof: Not applicableOpen item page →

Outward interval block LDL inertia certifier with pivot-inconclusive status

Definition

Input $n \geq 1$ , a nonempty family of Hermitian matrices in $C^{n \times n}$ enclosed by complex rectangles with real diagonal intervals and conjugate-paired off-diagonal rectangles, a simultaneous permutation of all $n$ positions, a partition of the permuted positions into consecutive pivot blocks of sizes one or two, the corresponding structural ordering, and a threshold $θ \in (0, 1]$ . The exact midpoint matrix is Hermitian. First run the exact-arithmetic branch of Sparse symmetric-indefinite block LDL* with threshold tests and failure status on that midpoint with this same ordering, block partition and threshold. If it reports pivot-failure, return pivot-inconclusive; this is only failure of this candidate plan.

For a successful candidate plan, independently initialize the interval active matrix from the family enclosure and process the same blocks. At a one-by-one pivot require its real interval to exclude zero and determine its sign. At a two-by-two pivot, outward-enclose its real determinant $a d - ∣ b ∣^{2}$ and trace $a + d$ . Use A Hermitian two-by-two pivot inertia is determined by determinant and trace signs: accept a negative determinant as inertia $(1, 1, 0)$ ; accept a positive determinant together with positive trace as $(2, 0, 0)$ , and with negative trace as $(0, 2, 0)$ . If these signs cannot be established, return pivot-inconclusive with the block index.

For each accepted block form its interval inverse from the scalar reciprocal or the adjugate divided by the determinant interval. Update the trailing Hermitian Schur complement by outward evaluation of $C - B D^{- 1} B^{*}$ . If a required denominator includes zero, an operation is undefined, an enclosure is non-finite, or Hermitian symmetry cannot be maintained, return pivot-inconclusive. At completion sum the certified pivot inertia triples and return certified-inertia with the count and factor/update record.

Every accepted pivot is nonsingular for every matrix represented by the current interval active matrix. A midpoint pivot failure, an interval pivot failure, or an unresolved sign never asserts that a family member is singular. The procedure makes no universal pivot-success or growth claim.

AlgorithmAlgorithm: Literature-sourcedProof: Not applicableOpen item page →

Interval Krawczyk linear system certifier with explicit statuses

Definition

Input $n \geq 1$ , a nonempty family of square matrices $A$ and right-hand sides $b$ enclosed by finite complex rectangles, a closed complex rectangle box $X \subset C^{n}$ , a point $x_{0} \in X$ , and dyadic point matrices $R, S \in C^{n \times n}$ with exact identities $R S = S R = I$ . The witness $S$ establishes that $R$ is nonsingular. No independence assumption on the actual family is required beyond its inclusion in the input boxes.

Outward-evaluate, over the full family boxes and $x \in X$ , the Krawczyk expression

K = x_{0} - R (A x_{0} - b) + (I - R A) (X - x_{0}) .

If any interval operation is not finite and defined, return inconclusive.

Compare the resulting enclosing rectangle box with $X$ by exact endpoint comparisons. If it is not contained in $X$ , return inconclusive. Otherwise outward-bound the maximum row sum of $∣ I - R A ∣$ uniformly over the family by a number $q$ . If this norm bound cannot be enclosed finitely, return existence-certified with uniqueness-inconclusive and no defect bound. If it is finite, return existence-certified; attach unique-certified for each fixed pair if the outward comparison certifies $q < 1$ , and otherwise attach uniqueness-inconclusive.

The enclosure in step 1 may be wider than the exact set of Krawczyk values; only successful inclusion produces a claim. A failed inclusion or a failed norm bound does not imply singularity.

AlgorithmAlgorithm: Literature-sourcedProof: Not applicablejudge pass (gpt-6-luna)Open item page →

Certified Hermitian eigenvalue intervals from residual and Gram bounds

Definition

Input $n \geq 1$ , a nonempty family of Hermitian $n \times n$ matrices enclosed by complex rectangles, a point matrix $V \in C^{n \times n}$ , a real diagonal matrix $Θ \in R^{n \times n}$ , and proposed nonnegative bounds $δ, ρ, M_{A}, M_{Θ}, τ$ . Treat point data as exact dyadics and the family as any subset of its enclosure.

With outward interval evaluation, enclose $V^{*} V - I$ and every $A V - V Θ$ for the full family. Form Frobenius upper bounds $d, r$ for these two matrices. Also form Frobenius upper bounds $m_{A}$ for every $A$ in the family and $m_{Θ}$ for $Θ$ . If any enclosure or square-root operation is non-finite, return inconclusive.
Verify by outward scalar comparisons that $d \leq δ < 1$ , $r \leq ρ$ , $m_{A} \leq M_{A}$ , $m_{Θ} \leq M_{Θ}$ , and that $1 - \sqrt{1 - δ} \leq τ$ . If any comparison is undecided or false, return inconclusive with the failed check. Otherwise outward-compute a finite upper bound $\overset{ˉ}{η} \geq ρ + (M_{A} + M_{Θ}) τ$ . For each increasingly sorted diagonal entry $θ_{(k)}$ , outward-compute finite endpoints $ℓ_{k} \leq θ_{(k)} - \overset{ˉ}{η}$ and $u_{k} \geq θ_{(k)} + \overset{ˉ}{η}$ , and set $I_{k} = [ℓ_{k}, u_{k}]$ . If the radius bound or any final endpoint cannot be enclosed finitely, return inconclusive; otherwise return certified with radius bound $\overset{ˉ}{η}$ and intervals $I_{1}, \dots, I_{n}$ .

The checks use the Frobenius norm as an upper bound for the operator 2-norm. An inconclusive check makes no statement about the true spectrum.

AlgorithmAlgorithm: Literature-sourcedProof: Not applicablejudge pass (gpt-6-luna)Open item page →

Finite precision point linear solve certificate with explicit status

Definition

Input $n \geq 1$ , stored finite real or complex square data $A \in C^{n \times n}$ , $b \in C^{n}$ , a proposed computed inverse $R \in C^{n \times n}$ , and a proposed computed solution $\hat{x} \in C^{n}$ . All stored entries are interpreted as exact dyadics. Use the operationwise arithmetic model with unit roundoff $u$ ; if $(n - 1) u \geq 1$ , return inconclusive before applying the rounded-residual bounds. The procedure validates the proposals; it does not assume that the solver which produced them is stable.

Set $g_{n} = (1 + 6 u) / (1 - (n - 1) u) - 1$ . Evaluate each column $a_{j}$ of $A$ through the operationwise model as ${\hat{m}}_{j} = fl (R a_{j})$ . If any operation returns range-failure, return range-failure with its first operation index. Compute an outward upper bound $v_{j}$ for $g_{n} ∥ R ∥_{F} ∥ a_{j} ∥_{2}$ , which by the rounded-linear-residual lemma bounds $∥ {\hat{m}}_{j} - R a_{j} ∥_{2}$ . Every dot product used for these allowances must complete successfully under the no-underflow model. Outward-evaluate $I - [{\hat{m}}_{1} \dots {\hat{m}}_{n}]$ and let $q$ be an outward upper bound for its Frobenius norm plus $\sqrt{\sum_{j} v_{j}^{2}}$ .
Evaluate $\hat{v} = fl (A \hat{x})$ and $\hat{w} = fl (\hat{v} - b)$ . Compute an outward upper bound $W$ for $g_{n} ∥ A ∥_{F} ∥ \hat{x} ∥_{2} + u (∥ \hat{v} ∥_{2} + ∥ b ∥_{2})$ , which bounds $∥ \hat{w} - (A \hat{x} - b) ∥_{2}$ . Evaluate $\hat{c} = fl (R \hat{w})$ and compute an outward upper bound $v_{c}$ for $g_{n} ∥ R ∥_{F} ∥ \hat{w} ∥_{2}$ , which bounds $∥ \hat{c} - R \hat{w} ∥_{2}$ . Let $r$ be an outward upper bound for

∥ \hat{c} ∥_{2} + ∥ R ∥_{F} W + v_{c} .

The Frobenius norm bounds $∥ R ∥_{2}$ .

All norm bounds, square roots, and final scalar operations are evaluated outward. If a bound cannot be enclosed finitely, return inconclusive. If $q \geq 1$ , return inconclusive with the computed bounds. If $q < 1$ , outward-compute $s \geq r / (1 - q)$ and return certified with the Euclidean ball $B (\hat{x}, s)$ .

The output range-failure describes failure of a requested floating operation. inconclusive means only that this validation did not prove a usable bound; it does not assert that $A$ is singular or that the proposed solution is inaccurate.

AlgorithmAlgorithm: Literature-sourcedProof: Not applicablejudge pass (gpt-6-luna)Open item page →

Uniform interval linear residual certificate with inconclusive status

Definition

Input $n \geq 1$ , nonempty families $A \subseteq C^{n \times n}$ and $b \subseteq C^{n}$ , each enclosed entrywise by finite complex rectangles, together with stored point proposals $R$ and $\hat{x}$ . The represented family need only be a subset of the supplied product of rectangles; correlations between entries may be discarded. All stored point data are exact dyadics.

Use outward rectangle operations to evaluate the expression DAGs

E (A) = I - R A, c (A, b) = R (b - A \hat{x})

over the full input rectangles. If an operation has no finite enclosure or returns a domain or range status, return inconclusive.

For each complex rectangle entry $X + i Y$ , outward-enclose its modulus by computing $\sqrt{X^{2} + Y^{2}}$ and taking the upper endpoint. Combine those bounds by outward sums of squares and square roots to obtain $q \geq \sup_{A \in A} ∥ E (A) ∥_{F}$ and $r \geq \sup_{A \in A, b \in b} ∥ c (A, b) ∥_{2}$ . If any modulus, sum, square root or final division has no finite outward result, return inconclusive. The Frobenius upper bound also bounds the operator 2-norm. If $q \geq 1$ , return inconclusive with $q, r$ . Otherwise return certified with the uniform residual data $(R, \hat{x}, q, r)$ and radius $r / (1 - q)$ , rounded outward if represented as a ball.

The interval DAG encloses every value for every admitted pair, including dependencies between repeated inputs because natural interval evaluation may enlarge the range. inconclusive makes no assertion that a member is singular.

TheoremStatement: AI-adaptedProof: AI-adaptedprecheck passjudge pass (gpt-6-luna)Open item page →

The finite disk cover validator returns a uniform resolvent bound on success

Statement

If the validator's input has $n \geq 1$ and Finite complex contour resolvent validator with cover and inconclusive statuses returns certified-resolvent-cover with bound $m$ , then every $A$ in the input family and every $z$ on the supplied contour segments satisfy that $z I - A$ is invertible and $∥ (z I - A)^{- 1} ∥_{\infty, C} \leq m$ . The result does not count eigenvalues inside the contour.

Facts & Assumptions

Given: The finite contour, disk assignments, matrix family and a successful validator return.

[F1]

Outward interval operations enclose all exact matrix and scalar quantities used by the validator (Outward-rounded operations are inclusion-isotone and enclose DAG evaluations).

[F2]

Certified disk bounds $e_{j}, δ_{A}, s_{j}$ with $e_{j} + s_{j} (r_{j} + δ_{A}) < 1$ imply a uniform resolvent bound on the covered contour (Diskwise Neumann certificates bound a complex matrix resolvent).

[F3]

The algorithm checks endpoint coverage and reports its maximum disk bound only after all strict inequalities succeed (Finite complex contour resolvent validator with cover and inconclusive statuses).

Proof

1.1givenF1F2F3algebra

By [F1], each reported $e_{j}, δ_{A}, s_{j}$ bounds the exact norm or family supremum it is intended to bound. The algorithm checks the disk endpoint conditions. Each whole assigned segment lies in its disk by convexity, so the disks cover every point of the contour. Its computed $q_{j} < 1$ and $m \geq \max_{j} s_{j} / (1 - q_{j})$ therefore satisfy all hypotheses and the bound comparison in [F2].

2.1F2step 1.1∎

Apply [F2] to obtain invertibility and the diskwise resolvent bound at every contour point and for every family member. Since each disk bound is at most $m$ , the returned uniform inequality follows. The theorem invoked in [F2] makes no eigenvalue-count assertion, so none is concluded here.

TheoremStatement: AI-adaptedProof: AI-adaptedprecheck passOpen item page →

The interval determinant sign certifier is sound and failure means unknown

Statement

If Outward Leibniz determinant sign and nonsingularity certifier returns nonsingular or all-singular for a real interval matrix family, the corresponding nonsingularity/sign or all-singular claim holds for every family member. An inconclusive result makes no claim about singularity.

Facts & Assumptions

Given: A nonempty real square matrix family represented by finite interval boxes and a completed algorithm return.

[F1]

When every operation returns a finite enclosure, outward interval DAG evaluation encloses the exact determinant range; a non-finite status asserts no finite DAG enclosure (Outward-rounded operations are inclusion-isotone and enclose DAG evaluations).

[F2]

An interval containing all determinants certifies nonsingularity when it excludes zero; the exact zero interval certifies singularity (An interval determinant excluding zero certifies nonsingularity and sign).

[F3]

The determinant algorithm evaluates the finite Leibniz formula and returns only the stated three statuses (Outward Leibniz determinant sign and nonsingularity certifier).

Proof

1.1givenF1F3algebra

Suppose the return is nonsingular or all-singular. By [F3], every operation in the finite Leibniz evaluation returned a finite enclosure, so [F1] gives $\det A \in D$ for every represented family member. If the return is nonsingular, then $0 \notin D$ ; if it is all-singular, then $D = {0}$ .

2.1F1F2F3step 1.1∎

Apply [F2] to $D$ in each of those two conclusive cases to obtain the claimed singularity or determinant-sign guarantee. By [F3], an inconclusive return occurs either after a non-finite operation, when [F1] asserts no finite determinant enclosure, or after a finite enclosure with $0 \in D$ and $D \neq {0}$ , when neither test in [F2] applies. In either branch the algorithm makes no singularity or sign claim.

TheoremStatement: AI-adaptedProof: AI-adaptedprecheck passjudge pass (gpt-6-luna)Open item page →

The interval block LDL certifier returns the exact inertia on success

Statement

If Outward interval block LDL inertia certifier with pivot-inconclusive status returns certified-inertia with $(n_{+}, n_{-}, n_{0})$ , every Hermitian matrix in its input family has exactly that inertia. A pivot-inconclusive return does not imply that any family member is singular.

Facts & Assumptions

Given: A nonempty Hermitian family with conjugate-symmetric interval enclosure, one fixed permutation and block plan, and a certified-inertia return.

[F1]

Outward interval DAG operations enclose exact sums, products, reciprocals and Schur updates (Outward-rounded operations are inclusion-isotone and enclose DAG evaluations).

[F2]

Each nonsingular Hermitian pivot block and its Schur complement contribute additively to inertia (Block LDL congruence adds the Hermitian pivot inertias).

[F3]

Nonsingular congruence, including a permutation congruence, preserves complex Hermitian inertia (Complex Hermitian inertia is invariant under nonsingular congruence).

[F4]

On success the algorithm's scalar and two-by-two sign tests certify the indicated nonzero pivot signs for every member of the current family enclosure (Outward interval block LDL inertia certifier with pivot-inconclusive status).

[F5]

For a two-by-two Hermitian pivot, a negative determinant gives inertia $(1, 1, 0)$ ; a positive determinant and trace sign give respectively $(2, 0, 0)$ or $(0, 2, 0)$ (A Hermitian two-by-two pivot inertia is determined by determinant and trace signs).

Proof

1.1givenF1F4induction

Induct over the pivot blocks. Initially the active interval matrix is the input family enclosure, so it encloses each original family member. If this holds before a block, [F1] makes the outward inverse and update enclose that member's exact pivot inverse and Schur complement; [F4] ensures the pivot is nonsingular throughout the family. Hence the enclosure invariant holds at the next block. The midpoint run only selects the candidate block plan; this interval induction is independent of its pivots.

2.1F2F3F4F5step 1.1algebra∎

A certified one-by-one pivot has the sign of its real interval. By [F5], each accepted two-by-two pivot has exactly its reported inertia. Applying [F2] successively to each pivot and its Schur complement, using congruence invariance [F3], proves that the sum returned at completion is the inertia of every original family member. If a test is unresolved the algorithm returns no inertia claim, and failure alone supplies no singularity conclusion.

TheoremStatement: AI-adaptedProof: AI-adaptedprecheck passOpen item page →

The interval Krawczyk certifier has the stated per-system guarantee

Statement

If Interval Krawczyk linear system certifier with explicit statuses returns existence-certified, every admitted system $A x = b$ has at least one solution in $X$ . If it also returns unique-certified, each fixed admitted pair has exactly one solution in $X$ . Inconclusive asserts neither existence nor singularity.

Facts & Assumptions

Given: The admitted matrix and right-hand-side families, box $X$ , $x_{0} \in X$ , a supplied inverse witness $S$ for $R$ , and an existence-certified run.

[F1]

Outward interval operations enclose their exact expression ranges (Outward-rounded operations are inclusion-isotone and enclose DAG evaluations).

[F2]

Krawczyk set inclusion gives existence, and a defect norm below one gives uniqueness (Krawczyk inclusion gives solutions and contraction gives uniqueness).

[F3]

On an existence-certified return the admitted inputs satisfy $R S = S R = I$ , and the algorithm checks that its outward Krawczyk enclosure lies in $X$ ; on a unique-certified return it also supplies an outward defect bound $q < 1$ (Interval Krawczyk linear system certifier with explicit statuses).

Proof

1.1givenF1F2F3algebra

Since $R S = S R = I$ , the supplied $R$ is invertible. By [F1], the computed enclosing box contains every exact value of $x_{0} - R (A x_{0} - b) + (I - R A) (x - x_{0})$ for each admitted pair and each $x \in X$ . Its successful inclusion in $X$ therefore implies the set $K^{*} (X)$ from [F2] is contained in $X$ .

2.1givenF2F3step 1.1∎

Apply [F2] to each fixed pair to obtain a solution in $X$ . If the run also reports unique-certified, [F3] supplies an outward row-sum bound with $∥ I - R A ∥_{\infty, C} \leq q < 1$ for every admitted $A$ , so the uniqueness clause of [F2] applies separately to every pair. If that strict bound is not returned, no uniqueness claim follows.

TheoremStatement: AI-adaptedProof: AI-adaptedprecheck passjudge pass (gpt-6-luna)Open item page →

The residual and orthogonality certifier encloses the full ordered spectrum

Statement

If Certified Hermitian eigenvalue intervals from residual and Gram bounds returns certified with outward radius bound $\overset{ˉ}{η}$ and intervals $I_{k}$ , then for every admitted Hermitian $A$ its $k$ -th increasing eigenvalue lies in $I_{k}$ . Each $I_{k}$ contains the symmetric interval $[θ_{(k)} - \overset{ˉ}{η}, θ_{(k)} + \overset{ˉ}{η}]$ . Inconclusive output makes no spectral claim.

Facts & Assumptions

Given: A nonempty Hermitian family and a certified algorithm return with validated bounds $δ, ρ, M_{A}, M_{Θ}, τ$ , outward radius bound $\overset{ˉ}{η}$ , and returned intervals $I_{k}$ .

[F1]

Outward interval calculations enclose every exact family residual, Gram defect and norm upper bound (Outward-rounded operations are inclusion-isotone and enclose DAG evaluations).

[F2]

The algorithm checks the hypotheses of the near-orthonormal residual enclosure and returns $\overset{ˉ}{η} \geq ρ + (M_{A} + M_{Θ}) τ$ with each $I_{k}$ containing $[θ_{(k)} - \overset{ˉ}{η}, θ_{(k)} + \overset{ˉ}{η}]$ (Certified Hermitian eigenvalue intervals from residual and Gram bounds, Residual and near-orthogonality data for an approximate Hermitian eigenbasis).

[F3]

Such residual and orthogonality data enclose every ordered Hermitian eigenvalue within $ρ + (M_{A} + M_{Θ}) τ$ (Near-orthonormal residual data enclose all ordered Hermitian eigenvalues).

[F4]

The operator 2-norm is at most the Frobenius norm (Spectral and Frobenius norms are unitarily invariant, are given by singular values, and satisfy the sharp rank comparison).

Proof

1.1F1F2F4algebra

By [F1], the reported interval bounds dominate the corresponding Frobenius norms for every admitted $A$ , and [F4] makes them upper bounds for the operator norms in the residual and orthogonality certificate. The algorithm accepts only if these bounds satisfy each inequality in that definition, including $δ < 1$ and $1 - \sqrt{1 - δ} \leq τ$ . Thus [F2] supplies valid certificate data uniformly for the whole family.

2.1F2F3step 1.1algebra∎

Apply [F3] to each $A$ . The theorem gives $∣ λ_{k} (A) - θ_{(k)} ∣ \leq ρ + (M_{A} + M_{Θ}) τ \leq \overset{ˉ}{η}$ for every increasing index $k$ , with the same validated radius bound for all members. Hence each eigenvalue lies in the centered interval contained in $I_{k}$ by [F2], and therefore lies in $I_{k}$ .

TheoremStatement: AI-adaptedProof: AI-adaptedprecheck passjudge pass (gpt-6-luna)Open item page →

The point linear solve certifier returns a sound solution ball on success

Statement

For exact stored dyadic $A, b, R, \hat{x}$ , if Finite precision point linear solve certificate with explicit status returns certified with ball $B (\hat{x}, s)$ , then $A$ is invertible and its unique solution $x$ to $A x = b$ belongs to that ball. A range-failure or inconclusive result makes no such claim.

Facts & Assumptions

Given: The exact input data and a certified return with outward bounds $q < 1$ , $r$ , and $s \geq r / (1 - q)$ .

[F1]

The point algorithm's rounded products and residuals satisfy the stated operationwise error allowances (Finite precision point linear solve certificate with explicit status, Rounded matrix products give certified linear and normal-equation residual allowances).

[F2]

Outward interval DAG evaluation encloses every exact operation and its range is isotone (Outward-rounded operations are inclusion-isotone and enclose DAG evaluations).

[F3]

Usable residual data imply a unique solution within $r / (1 - q)$ (A uniform approximate inverse and residual enclose every linear solution).

Proof

1.1F1F2algebra

On a successful run, the columnwise rounded products enclose every column of $R A$ with Euclidean errors at most $v_{j}$ , by [F1]. The Frobenius error between the rounded product matrix and $R A$ is therefore at most $\sqrt{\sum_{j} v_{j}^{2}}$ . Outward soundness [F2] encloses $I - \hat{R A}$ , so the reported $q$ bounds $∥ I - R A ∥_{2}$ by the triangle inequality and $∥ M ∥_{2} \leq ∥ M ∥_{F}$ .

1.2F1F2algebra

The rounded residual allowance $W$ bounds $∥ \hat{w} - (A \hat{x} - b) ∥_{2}$ and the rounded product allowance $v_{c}$ bounds $∥ \hat{c} - R \hat{w} ∥_{2}$ by [F1]. Thus $∥ R (b - A \hat{x}) ∥_{2} \leq ∥ \hat{c} ∥_{2} + ∥ R ∥_{2} W + v_{c} \leq r$ , where [F2] makes each reported upper bound outward and $∥ R ∥_{2} \leq ∥ R ∥_{F}$ .

2.1givenF3step 1.1step 1.2algebra∎

These are usable point residual certificate data with $q < 1$ . By [F3] the system has a unique solution and $∥ x - \hat{x} ∥_{2} \leq r / (1 - q) \leq s$ . The latter inequality is exactly the returned ball membership.

TheoremStatement: AI-adaptedProof: AI-adaptedprecheck passjudge pass (gpt-6-luna)Open item page →

The uniform interval residual certifier is sound on success

Statement

If Uniform interval linear residual certificate with inconclusive status returns certified with $(R, \hat{x}, q, r)$ , then every $(A, b)$ in the admitted families has a unique solution and its distance from $\hat{x}$ is at most $r / (1 - q)$ . Inconclusive output asserts no such conclusion.

Facts & Assumptions

Given: Nonempty matrix and right-hand-side families enclosed by the supplied rectangles and a successful algorithm return with $q < 1$ .

[F1]

Every exact family value in a finite interval expression DAG is enclosed by its outward result (Outward-rounded operations are inclusion-isotone and enclose DAG evaluations).

[F2]

Frobenius norm bounds the induced Euclidean operator norm (Spectral and Frobenius norms are unitarily invariant, are given by singular values, and satisfy the sharp rank comparison).

[F3]

The reported tuple is uniform residual certificate data (Uniform interval linear residual certificate with inconclusive status, Verified point and uniform linear residual certificate data).

[F4]

Usable uniform residual data give a unique solution and the stated error radius (A uniform approximate inverse and residual enclose every linear solution).

Proof

1.1F1F2F3algebra

By [F1], the interval DAGs for $I - R A$ and $R (b - A \hat{x})$ enclose these expressions simultaneously for every admitted $A, b$ . The component modulus bounds, sums of squares and square roots therefore bound their Frobenius or Euclidean norms uniformly. By [F2], the first Frobenius bound also bounds $∥ I - R A ∥_{2}$ . Thus the returned $q, r$ satisfy the inequalities in the uniform residual certificate definition.

2.1givenF3F4step 1.1∎

The run returns certified only with $q < 1$ . Apply [F4] to the uniform certificate: for every admitted pair there is a unique solution $x_{A} (b)$ and $∥ x_{A} (b) - \hat{x} ∥_{2} \leq r / (1 - q)$ .

AlgorithmAlgorithm: Literature-sourcedProof: Not applicablejudge pass (gpt-6-luna)Open item page →

Budgeted ordered Hermitian eigenvalue bisection by verified inertia

Definition

Input $n \geq 1$ , a nonempty family of Hermitian $n \times n$ matrices enclosed by conjugate-symmetric interval rectangles, tolerance $ε > 0$ , a total query budget $B \in N_{0}$ , and a fixed ordering, block plan and threshold $θ \in (0, 1]$ for the interval inertia certifier. Interpret all interval endpoints and shifts exactly.

Outward-compute $M \geq \sup_{A} ∥ A ∥_{F}$ by bounding each entry modulus and summing their squares. If a finite bound cannot be obtained, return inconclusive with no eigenvalue intervals. Otherwise initialize, for each increasing index $k = 1, \dots, n$ , the bracket $I_{k} = [- M, M]$ and successful-query count $s_{k} = 0$ . The Frobenius eigenvalue bound guarantees that these brackets contain every eigenvalue of every family member.
Repeat while fewer than $B$ total queries have been used and there is an index whose bracket width exceeds $ε$ and which has not been marked blocked. Choose the least such index $k$ . Query its exact midpoint $τ$ . Run Outward interval block LDL inertia certifier with pivot-inconclusive status on the shifted family ${A - τ I : A \in A}$ with the fixed plan. If the result is pivot-inconclusive, or its certified inertia has nonzero zero-count, mark this index blocked and leave $I_{k}$ unchanged. Otherwise set $ν = n_{-}$ , the certified number of negative eigenvalues. If $ν \geq k$ , replace the upper endpoint of $I_{k}$ by $τ$ ; if $ν < k$ , replace the lower endpoint by $τ$ . Increase $s_{k}$ by one. A certified update halves the bracket width. Stop when the query budget is used or no such index exists.
Return every current bracket with status enclosed when its width is at most $ε$ , inconclusive if its index was blocked, or budget-exhausted if the total budget ended first. A zero-width initial bracket is already complete. Neither blocked pivots nor exhausted budget alter an existing bracket.

The algorithm does not perturb a shift to force an LDL pivot and does not infer singularity from a failed factorization. It returns uniform outer intervals for a family; it does not identify eigenvalue branches across parameter values.

TheoremStatement: AI-adaptedProof: AI-adaptedprecheck passjudge pass (gpt-6-luna)Open item page →

The ordered Hermitian bisection certifier returns valid intervals or an inconclusive status

Statement

For every completed run of Budgeted ordered Hermitian eigenvalue bisection by verified inertia on a family of $n \geq 1$ dimensional Hermitian matrices, each returned interval for index $k \in {1, \dots, n}$ contains $λ_{k} (A)$ for every admitted matrix $A$ . A blocked or budget-exhausted result preserves the same enclosure guarantee but may have width greater than the requested tolerance. Failure to certify a shift is not evidence of a singular family member.

Facts & Assumptions

Given: A nonempty Hermitian family with sound finite interval enclosure, positive tolerance and a finite query budget.

[F1]

Outward interval bounds enclose every family entry and every computed norm upper bound (Outward-rounded operations are inclusion-isotone and enclose DAG evaluations).

[F2]

Every eigenvalue lies in the interval given by a uniform Frobenius norm bound (Hermitian eigenvalues lie within a certified Frobenius bound).

[F3]

A successful interval LDL inertia result is the exact uniform inertia for every shifted family member (The interval block LDL certifier returns the exact inertia on success).

[F4]

Inertia-guided midpoint updates preserve ordered eigenvalue brackets, and an inconclusive query leaves its bracket unchanged (Certified inertia counts maintain ordered eigenvalue brackets).

Proof

1.1givenF1F2algebra

If the interval norm calculation succeeds, [F1] makes its returned $M$ an upper bound for every $∥ A ∥_{F}$ . By [F2], every eigenvalue of every member lies in $[- M, M]$ , so all initial brackets are valid.

1.2givenF3F4algebra

At a successful shift, [F3] supplies one inertia for every $A - τ I$ and its zero count is checked to be zero. Its negative count is therefore exactly the number of eigenvalues of each $A$ below $τ$ . The algorithm's update is the successful query of [F4]; on pivot failure or a zero pivot it leaves the interval unchanged, which is the inconclusive branch of [F4].

2.1givenF4step 1.1step 1.2induction∎

Apply [F4] to each index, treating later unexecuted queries after a blocked index or budget exhaustion as no-op inconclusive queries. Each bracket therefore continues to contain the corresponding ordered eigenvalue for every family member. Certified updates halve its width, while statuses only describe why the requested tolerance or query count may not have been reached.

5 · Examples, counterexamples and false statements

None yet.