LemmaStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedprecheck pass

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 strong RRQR column swap multiplies selected volume by its score

Statement

Let $A \in F^{m \times n}$ have full column rank, $m \geq n$ , and let $A Π = Q R$ be a full QR factorization, with $Q \in F^{m \times m}$ unitary and $R \in F^{m \times n}$ upper trapezoidal. Partition $R = [\begin{array}{cc} R_{11} & R_{12} \\ 0 & R_{22} \end{array}]$ after the first $k$ rows and columns, where $R_{11} \in F^{k \times k}$ is nonsingular and $1 \leq k < n$ . Write $X = R_{11}^{- 1} R_{12}$ , $ω_{i} = ∥ e_{i}^{*} R_{11}^{- 1} ∥_{2}$ , and $γ_{j} = ∥ R_{22} (:, j) ∥_{2}$ . Use local one-based QR positions and define the original column labels $π (s)$ by $(A Π) (:, s) = A (:, π (s))$ . Let $J = {π (1), \dots, π (k)}$ be the selected set of $k$ columns and define its volume by $vol (A (:, J)) = \det (A (:, J)^{*} A (:, J))^{1 / 2}$ . For $1 \leq i \leq k$ and $1 \leq j \leq n - k$ , replacing selected column $π (i)$ by trailing column $π (k + j)$ changes this volume by the factor $\frac{vol (A (:, (J ∖ {π (i)}) \cup {π (k + j)}))}{vol (A (:, J))} = (∣ X_{i j} ∣^{2} + (ω_{i} γ_{j})^{2})^{1 / 2} .$

Facts & Assumptions

Given: A full-column-rank matrix, its partitioned QR factorization, and indices $i, j$ as above.

[F1]

Strong rank-revealing QR with finite swaps and explicit statuses defines $X$ , $ω_{i}$ , $γ_{j}$ , and the score used to select a swap.

Proof

1.1F1construct

Apply $Q^{*}$ to the selected columns and the candidate trailing column. The selected matrix becomes $C = R_{11}$ in the top $k$ rows. After replacing column $i$ , the top block is $C^{'} = R_{11} S$ , where $S$ is the identity with column $i$ replaced by column $j$ of $X$ ; the lower block has only column $i$ nonzero, equal to $c = R_{22} (:, j)$ . Hence the replaced Gram matrix is $(C^{'})^{*} C^{'} + ∥ c ∥_{2}^{2} e_{i} e_{i}^{*}$ . If $X_{i j} \neq 0$ , then $S$ is nonsingular, $\det S = X_{i j}$ , and row $i$ of $(C^{'})^{- 1} = S^{- 1} R_{11}^{- 1}$ is row $i$ of $R_{11}^{- 1}$ divided by $X_{i j}$ .

2.1step 1.1algebra

For any nonsingular Gram matrix $G$ and vector $u$ , factor $G + u u^{*} = G (I + G^{- 1} u u^{*})$ . Multilinearity of the determinant gives $\det (I + a b^{*}) = 1 + b^{*} a$ : terms choosing two updated columns vanish because both are proportional to $a$ . Hence $\det (G + u u^{*}) = \det (G) (1 + u^{*} G^{- 1} u)$ . Apply this identity to the Gram matrix in step 1.1 with $G = (C^{'})^{*} C^{'}$ and $u = ∥ c ∥_{2} e_{i}$ . Since $(C^{'})^{- 1}$ has row $i$ equal to row $i$ of $R_{11}^{- 1}$ divided by $X_{i j}$ , $e_{i}^{*} G^{- 1} e_{i} = ω_{i}^{2} / ∣ X_{i j} ∣^{2}$ . The determinant is therefore $∣ \det R_{11} ∣^{2} ∣ X_{i j} ∣^{2} (1 + ∥ c ∥_{2}^{2} ω_{i}^{2} / ∣ X_{i j} ∣^{2}) = ∣ \det R_{11} ∣^{2} (∣ X_{i j} ∣^{2} + (ω_{i} γ_{j})^{2})$ . The original selected volume squared is $∣ \det R_{11} ∣^{2}$ , so taking the nonnegative square root gives the formula when $X_{i j} \neq 0$ .

3.1step 2.1algebra∎

Both squared volumes and the right-hand side in step 2.1 are continuous in $X_{i j}$ . Perturbing $X_{i j}$ to nonzero values and taking a limit proves the same identity when $X_{i j} = 0$ .

Depends on

Strong rank-revealing QR with finite swaps and explicit statuses

Used by

The strong RRQR swap rule terminates after finitely many swaps Theorem

Dependency tree · two levels

4 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

Ming Gu and Stanley C. Eisenstat, Efficient Algorithms for Computing a Strong Rank-Revealing QR Factorization, Lemma 3.1 (standard reference, not scraped)
Wen-Wei Lin, Lecture Notes of Matrix Computations, §3.2.2 (standard reference, not scraped)