TheoremStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedprecheck passjudge pass (gpt-6-luna)

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.

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.

Depends on

Used by

Dependency tree · two levels

14 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources

Siegfried M. Rump, Verification methods: Rigorous results using floating-point arithmetic, Acta Numerica 19 (2010), §10.5 (standard reference, not scraped)
Nicholas J. Higham, Numerical Linear Algebra and Matrix Analysis, MIMS EPrint 2015.103, §1 (standard reference, not scraped)